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

协作研究：SaTC：核心：大型：构建和部署经过验证的 JavaScript 运行时

• 批准号: 2120696
• 负责人: Hovav Shacham
• 金额: $ 172.99万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2120696&HistoricalAwards=false
• 关键词: Collaborative; Research; SaTC; CORE; Large

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.

浏览器运行复杂的Web应用程序现代社会所依赖。浏览器供应商使用Just-In-time（JIT）编译器将Web应用程序代码（用JavaScript编写的Web应用程序代码）变成优化的计算机代码，以使Web应用程序有效地在用户机上有效运行。不幸的是，JavaScript JIT中的错误已成为对Web平台安全性的最大威胁和与Web连接的设备的最危险的攻击表面。 JavaScript JITS中的错误可以并且已被攻击者对目标用户（包括边缘化和高危人群的成员）进行利用。该项目的目的是构建和部署更安全的JavaScript JIT。为此，调查人员将开发新技术，框架和原则，（1）帮助浏览器开发人员构建可证明安全的JIT编译器，并且（2）不会引起传统上与高保险软件相关的高成本和开发时间表。如果成功，该项目将提高每天浏览网络的数亿人的安全性。 该项目将：（1）经验评估JIT安全性，确定最容易受到攻击者的JIT组件，并且对浏览器性能最重要； （2）正式将安全性和正确性对JIT的各个部分意味着什么； （3）修改和扩展现有的JIT编译器以查找和修复错误，并为当今的主动攻击下的组件提供正式保证；最后，（4）通过设计和构建可扩展，可维护和安全的新型JavaScript口译员和编译器，重新考虑从头开始执行JavaScript程序的方式。该项目将在编程语言和验证框架的设计中产生新的创新，结果将使浏览器开发人员能够用更少的工作编写更安全的JIT编译器。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子和更广泛影响的评估来通过评估来获得支持的审查。

项目成果

Going beyond the Limits of SFI: Flexible and Secure Hardware-Assisted In-Process Isolation with HFI

• DOI: 10.1145/3582016.3582023
• 发表时间: 2023-03
• 期刊: Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3
• 作者: Shravan Narayan;Tal Garfinkel;Mohammadkazem Taram;Joey Rudek;D. Moghimi;Evan Johnson;Chris Fallin

SoK: Practical Foundations for Software Spectre Defenses

SoK：软件幽灵防御的实用基础

• 发表时间: 2022
• 期刊: 43rd IEEE Symposium on Security and Privacy
• 作者: Sunjay Cauligi, Craig Disselkoen

Flux: Liquid Types for Rust

助焊剂：用于防锈的液体类型

• DOI: 10.1145/3591283
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Lehmann, Nico;Geller, Adam T.;Vazou, Niki;Jhala, Ranjit
• 通讯作者: Jhala, Ranjit

Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI

无需纳税的隔离：WebAssembly 和 SFI 的近乎零成本转换

• DOI: 10.1145/3498688
• 发表时间: 2022
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Kolosick, Matthew;Narayan, Shravan;Johnson, Evan;Watt, Conrad;LeMay, Michael;Garg, Deepak;Jhala, Ranjit;Stefan, Deian
• 通讯作者: Stefan, Deian

WaVe: a verifiably secure WebAssembly sandboxing runtime

• DOI: 10.1109/sp46215.2023.10179357
• 发表时间: 2023-05
• 期刊: 2023 IEEE Symposium on Security and Privacy (SP)
• 作者: Evan Johnson;Evan Laufer;Zijie Zhao;D. Gohman;Shravan Narayan;S. Savage;D. Stefan;Fraser Brown-Fraser-Brow