Collaborative Research: SaTC: CORE: Large: Building and Deploying a Verified JavaScript Runtime

浏览器运行现代社会所依赖的复杂的Web应用程序。浏览器供应商竭尽全力让Web应用程序在用户机器上高效运行，他们使用实时(JIT)编译器将用JavaScript编写的Web应用程序代码转换为优化的机器码。不幸的是，JavaScript JIT中的漏洞已经成为网络平台安全的最大威胁，也是网络连接设备最危险的攻击面。攻击者可以而且已经利用JavaScript JIT中的漏洞来瞄准用户，包括边缘人群和高危人群的成员。该项目的目标是构建和部署更安全的JavaScript JIT。为此，调查人员将开发新的技术、框架和原则，以(1)帮助浏览器开发人员构建可证明安全的JIT编译器，(2)不会招致传统上与高保证软件相关的高成本和开发时间表。如果成功，这个项目将提高数亿每天上网的人的安全。该项目将：(1)经验性地评估JIT安全性，确定最容易受到攻击者攻击和对浏览器性能最关键的JIT组件；(2)正式确定安全和正确性对于JIT的各个部分意味着什么；(3)修改和扩展现有的JIT编译器以发现并修复错误，并为当前受到主动攻击的组件提供正式的安全保证；最后，(4)通过设计和构建可扩展、可维护和安全的新的Java解释器和编译器，从根本上重新思考浏览器执行Java程序的方式。该项目将在编程语言和验证框架的设计方面产生新的创新，从而使浏览器开发人员能够以更少的工作编写更安全的JIT编译器。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Browsers run the complex Web applications modern society relies on. Browser vendors go to great lengths to make Web applications run efficiently on user machines, using just-in-time (JIT) compilers that turns Web application code, written in JavaScript, into optimized machine code. Unfortunately, bugs in JavaScript JITs have emerged as the single largest threat to web platform security and the most dangerous attack surface of web-connected devices. Bugs in JavaScript JITs can and have been exploited by attackers to target users, including members of marginalized and at-risk populations. The goal of this project is to build and deploy more secure JavaScript JITs. To this end, the investigators will develop new techniques, frameworks, and principles that (1) help browser developers build JIT compilers that are provably secure and (2) don't incur the high costs and development timelines traditionally associated with high-assurance software. If successful, this project will improve security for the hundreds of millions of people who surf the web every day. The project will: (1) empirically evaluate JIT security, identifying the JIT components that are most vulnerable to attackers and most crucial to browser performance; (2) formalize what security and correctness mean for various parts of the JIT; (3) modify and extend existing JIT compilers to find and fix bugs, and provide formal guarantees of security for components under active attack today; and, finally, (4) rethink the way that browsers execute JavaScript programs from the ground up, by designing and building new JavaScript interpreters and compilers that are extensible, maintainable, and secure. The project will yield new innovations in the design of programming languages and verification frameworks, and as a result will empower browser developers to write safer JIT compilers with less work.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.