TWC: Medium: Towards a Formally Verified Web Browser
TWC:媒介:迈向正式验证的 Web 浏览器
基本信息
- 批准号:1228967
- 负责人:
- 金额:$ 111万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Standard Grant
- 财政年份:2012
- 资助国家:美国
- 起止时间:2012-10-01 至 2017-09-30
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
The web browser is ubiquitous and indispensable. It runs applicationslike social networking, business productivity, and online banking, andpromises isolation policies that keep these applications secure whenrun side-by-side. Because of its crucial role, we would like thebrowser to be robust and secure against attack; but in fact browsersare fragile. They are complex pieces of software with rich featuresthat allow for flexibility and programmability, and even small bugscan make the browser vulnerable to attack. Indeed, browservulnerabilities have been used to infiltrate the internal networks ofAmerican defense contractors and leading tech firms. Attempts toimprove browser security are often ad-hoc engineering efforts; andeven when formal guarantees are provided, they come in the form ofproofs over a model or idealization of the browser, not the browseritself. A buggy implementation can invalidate intended guarantees andleave users open to attack.The goal of this project is to build a browser inside the Coq proofassistant, along with a proof of its correctness. Unlike previousresearch efforts, the proof covers the actual browser implementationrather than a model or abstraction. This provides extremely strong,precise guarantees about the security properties of the browser. Theproof is made tractable by focusing the verification effort to a smallbrowser kernel, and running legacy code in a sandbox to renderweb pages. In this way, the browser can provide meaningful isolationguarantees even when the legacy code that renders web pages isuntrusted and potentially buggy. This project will provide:* For users of the web, browsers that are more reliable and secure;* For software developers, a new approach for developing high-assurance systems;* For researchers, a framework for formally reasoning about security policies;* For students, security and formal methods education.
网络浏览器无处不在且不可或缺。它运行社交网络、企业生产力和在线银行等应用程序,并承诺隔离策略,以确保这些应用程序并行运行时的安全。由于其至关重要的作用,我们希望浏览器能够稳健且安全地抵御攻击;但事实上浏览器是脆弱的。它们是复杂的软件,具有丰富的功能,具有灵活性和可编程性,即使是小错误也会使浏览器容易受到攻击。事实上,浏览器漏洞已被用来渗透美国国防承包商和领先科技公司的内部网络。提高浏览器安全性的尝试通常是临时工程工作;即使提供了正式的保证,它们也以浏览器模型或理想化的证明形式出现,而不是浏览器本身。 有缺陷的实现可能会使预期的保证失效,并使用户容易受到攻击。该项目的目标是在 Coq 证明助手中构建一个浏览器,并证明其正确性。与之前的研究工作不同,该证明涵盖了实际的浏览器实现,而不是模型或抽象。 这为浏览器的安全特性提供了极其有力、精确的保证。通过将验证工作集中到小型浏览器内核,并在沙箱中运行遗留代码来渲染网页,使证明变得容易处理。通过这种方式,即使呈现网页的遗留代码不受信任并且可能存在错误,浏览器也可以提供有意义的隔离保证。该项目将提供:* 对于网络用户来说,浏览器更加可靠和安全;* 对于软件开发人员来说,一种开发高保证系统的新方法;* 对于研究人员来说,一个用于正式推理安全策略的框架;* 对于学生、安全和正规方法教育。
项目成果
期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
数据更新时间:{{ journalArticles.updateTime }}
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Sorin Lerner其他文献
Automated refinement checking of concurrent systems
并发系统的自动细化检查
- DOI:
10.1109/iccad.2007.4397284 - 发表时间:
2007-11-05 - 期刊:
- 影响因子:0
- 作者:
Sudipta Kundu;Sorin Lerner;Rajesh K. Gupta - 通讯作者:
Rajesh K. Gupta
Addressing common crosscutting problems with Arcum
使用 Arcum 解决常见横切问题
- DOI:
10.1145/1512475.1512489 - 发表时间:
2008-11-09 - 期刊:
- 影响因子:0
- 作者:
Macneil Shonle;W. Griswold;Sorin Lerner - 通讯作者:
Sorin Lerner
How do Haskell programmers debug?
Haskell 程序员如何调试?
- DOI:
10.1007/978-3-642-34407-7_5 - 发表时间:
2023 - 期刊:
- 影响因子:0
- 作者:
Sarah E. Chasins;Elena Glassman;Joshua Sunshine;Lisa Huang;Elizaveta Pertseva;Michael J. Coblenz;Sorin Lerner - 通讯作者:
Sorin Lerner
Establishing Browser Security Guarantees through Formal Shim Verification
通过正式的 Shim 验证建立浏览器安全保证
- DOI:
10.1016/s1571-0661(05)01135-7 - 发表时间:
2012-08-08 - 期刊:
- 影响因子:0
- 作者:
Dongseok Jang;Zachary Tatlock;Sorin Lerner - 通讯作者:
Sorin Lerner
WitchDoctor: IDE support for real-time auto-completion of refactorings
WitchDoctor:IDE 支持实时自动完成重构
- DOI:
10.1109/icse.2012.6227191 - 发表时间:
2012-06-02 - 期刊:
- 影响因子:0
- 作者:
S. Foster;W. Griswold;Sorin Lerner - 通讯作者:
Sorin Lerner
Sorin Lerner的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Sorin Lerner', 18)}}的其他基金
Collaborative Research: SHF: Small: Data-Driven Lemma Synthesis for Interactive Proofs
协作研究:SHF:小型:交互式证明的数据驱动引理合成
- 批准号:
2220892 - 财政年份:2022
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
SHF: Medium: Generating Correctness Proofs with Neural Networks
SHF:中:使用神经网络生成正确性证明
- 批准号:
1955457 - 财政年份:2020
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
CPS: Synergy: Towards Foundational Verification of Cyber-Physical Systems
CPS:协同:迈向网络物理系统的基础验证
- 批准号:
1544757 - 财政年份:2015
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
SHF:Small: Bringing Extensibility and Performance to Verified Compilers
SHF:Small:为经过验证的编译器带来可扩展性和性能
- 批准号:
1219172 - 财政年份:2012
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
SHF: Small: Application Shrinking for Reducing Energy Consumption
SHF:小型:缩小应用范围以降低能耗
- 批准号:
1018632 - 财政年份:2010
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
CPA-CPL: Scalable Analysis for Concurrent Programs
CPA-CPL:并发程序的可扩展分析
- 批准号:
0811512 - 财政年份:2008
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
CAREER: Automatically Generating and Processing Program Analyses and Optimizations
职业:自动生成和处理程序分析和优化
- 批准号:
0644306 - 财政年份:2007
- 资助金额:
$ 111万 - 项目类别:
Continuing Grant
相似国自然基金
基于挥发性分布和氧化校正的大气半/中等挥发性有机物来源解析方法构建
- 批准号:42377095
- 批准年份:2023
- 资助金额:49 万元
- 项目类别:面上项目
基于机器学习和经典电动力学研究中等尺寸金属纳米粒子的量子表面等离激元
- 批准号:22373002
- 批准年份:2023
- 资助金额:50 万元
- 项目类别:面上项目
中等质量黑洞附近的暗物质分布及其IMRI系统引力波回波探测
- 批准号:12365008
- 批准年份:2023
- 资助金额:32 万元
- 项目类别:地区科学基金项目
复合低维拓扑材料中等离激元增强光学响应的研究
- 批准号:12374288
- 批准年份:2023
- 资助金额:52 万元
- 项目类别:面上项目
中等垂直风切变下非对称型热带气旋快速增强的物理机制研究
- 批准号:42305004
- 批准年份:2023
- 资助金额:30 万元
- 项目类别:青年科学基金项目
相似海外基金
TWC: Medium: Collaborative: Towards a Binary-Centric Framework for Cyber Forensics in Enterprise Environments
TWC:媒介:协作:迈向企业环境中以二进制为中心的网络取证框架
- 批准号:
1732143 - 财政年份:2016
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
TWC: Medium: Collaborative: Towards a Binary-Centric Framework for Cyber Forensics in Enterprise Environments
TWC:媒介:协作:迈向企业环境中以二进制为中心的网络取证框架
- 批准号:
1409534 - 财政年份:2014
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
TWC: Medium: Collaborative: Towards a Binary-Centric Framework for Cyber Forensics in Enterprise Environments
TWC:媒介:协作:迈向企业环境中以二进制为中心的网络取证框架
- 批准号:
1409668 - 财政年份:2014
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
TWC: Medium: Collaborative: Towards Securing Coupled Financial and Power Systems in the Next Generation Smart Grid
TWC:中:协作:确保下一代智能电网中耦合金融和电力系统的安全
- 批准号:
1229008 - 财政年份:2012
- 资助金额:
$ 111万 - 项目类别:
Standard Grant
TWC: Medium: Collaborative: Towards Secure, Robust, and Usable Gesture-Based Authentication
TWC:媒介:协作:迈向安全、稳健且可用的基于手势的身份验证
- 批准号:
1228842 - 财政年份:2012
- 资助金额:
$ 111万 - 项目类别:
Standard Grant