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

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

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.