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

点击翻译按钮获取中文摘要

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.