SaTC: CORE: Medium: Secure and Formally-verified Low-level Languages

SaTC:核心:中:安全且经过正式验证的低级语言

基本信息

  • 批准号:
    2247088
  • 负责人:
  • 金额:
    $ 120万
  • 依托单位:
  • 依托单位国家:
    美国
  • 项目类别:
    Standard Grant
  • 财政年份:
    2023
  • 资助国家:
    美国
  • 起止时间:
    2023-10-01 至 2027-09-30
  • 项目状态:
    未结题

项目摘要

Our modern computing infrastructure, including the Internet and multitude of applications that run on our phones and in data centers, relies on many low-level software systems to function correctly. Low-level software includes things like operating systems and the tools, such as programming language compilers, that are used by software developers to build those applications. Flaws in the design of low-level software, or bugs in its implementation, can lead to system crashes, security vulnerabilities, or incorrect results that can be very costly to individuals, businesses, and scientific or educational institutions. The research conducted as part of this project will investigate how to improve the security and reliability of low-level software. The research focuses on a specific piece of the modern software infrastructure (something called LLVM IR, an industrial-strength bit of compiler infrastructure that is widely used in industry and academia), and develop a formal, computer-checkable, mathematical model of its behaviors. That model will be used to uncover flaws in the infrastructure, and as an aid to implementing correct systems using it. Because such systems are ubiquitous, improving their security and reliability can potentially have significant positive impact for society as a whole. This project will also develop educational resources suitable for teaching the underlying theory and techniques to software developers who use this infrastructure.The project will build on and extend the capabilities of Vellvm--the "Verified LLVM IR"--a formalization of the LLVM compiler infrastructure implemented in the Coq interactive theorem prover. Because the LLVM ecosystem supports many source languages (C, C++, Rust, Haskell, among others) and target platforms (including almost all modern processors), it is a natural fulcrum to amplify the impact of formal modeling and verification efforts. The research conducted here will have three main thrusts: (1) Improving Vellvm's fidelity and completeness with respect to the LLVM IR by extending the suite of supported LLVM IR constructs, developing a new memory model, and concurrency semantics that enable optimizations unavailable previousl; (2) Designing abstractions that facilitate relational reasoning about LLVM IR programs. These abstractions will take the form of a collection of domain-specific logics for reasoning about LLVM IR code at various levels of abstraction; (3) applying the Vellvm framework to build tools that help identify undefined behaviors and mitigate security vulnerabilities in LLVM IR programs. To achieve these goals, the proposed research will develop novel reasoning and proof automation techniques that are applicable to low-level program semantics. All of the developments will be implemented and verified using the Coq interactive theorem prover, yielding a high-degree of confidence in the results.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.
我们的现代计算基础设施,包括互联网以及在手机和数据中心运行的众多应用程序,都依赖于许多低级软件系统来正常运行。 低级软件包括操作系统和工具,如编程语言编译器,软件开发人员用来构建这些应用程序。 低级软件设计中的缺陷或其实现中的错误可能导致系统崩溃、安全漏洞或错误结果,这对个人、企业和科学或教育机构来说可能是非常昂贵的。 作为该项目的一部分进行的研究将调查如何提高低级软件的安全性和可靠性。 该研究侧重于现代软件基础设施的一个特定部分(称为LLVM IR,一种广泛用于工业和学术界的工业强度编译器基础设施),并开发其行为的正式,计算机可检查的数学模型。 该模型将用于发现基础设施中的缺陷,并作为使用该模型实施正确系统的辅助工具。由于此类系统无处不在,因此提高其安全性和可靠性可能会对整个社会产生重大的积极影响。 该项目还将开发教育资源,用于向使用该基础设施的软件开发人员教授基础理论和技术。该项目将建立并扩展Vellvm的功能-“Verified LLVM IR”-在Coq交互式定理证明器中实现的LLVM编译器基础设施的形式化。由于LLVM生态系统支持许多源语言(C、C++、Rust、Haskell等)和目标平台(包括几乎所有现代处理器),因此它是放大形式化建模和验证工作影响的自然支点。这里进行的研究将有三个主要目标:(1)通过扩展支持LLVM IR结构的套件,开发新的内存模型和并发语义来提高Vellvm对LLVM IR的保真度和完整性,从而实现以前无法实现的优化;(2)设计便于LLVM IR程序的关系推理的抽象。这些抽象将采取特定于域的逻辑集合的形式,用于在各种抽象级别上对LLVM IR代码进行推理;(3)应用Vellvm框架来构建工具,以帮助识别未定义的行为并减轻LLVM IR程序中的安全漏洞。 为了实现这些目标,拟议的研究将开发新的推理和证明自动化技术,适用于低层次的程序语义。 所有的开发都将使用Coq交互式定理证明器进行实施和验证,从而对结果产生高度的信心。该奖项反映了NSF的法定使命,并通过使用基金会的知识价值和更广泛的影响审查标准进行评估,被认为值得支持。

项目成果

期刊论文数量(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 }}

Stephan Zdancewic其他文献

Stephan Zdancewic的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('Stephan Zdancewic', 18)}}的其他基金

REU Site: Research Experience for undergraduates in Programming Languages (REPL)
REU 网站:编程语言本科生研究经验 (REPL)
  • 批准号:
    2244494
  • 财政年份:
    2023
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
Student Travel for Programming Languages Mentoring Workshop at ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 2019 (PLMW@POPL)
2019 年 ACM SIGACT-SIGPLAN 编程语言原理研讨会学生编程语言指导研讨会 (PLMW@POPL)
  • 批准号:
    1841603
  • 财政年份:
    2018
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
NSF Student Travel Grant for 2018 Programming Languages
NSF 2018 年编程语言学生旅行补助金
  • 批准号:
    1749155
  • 财政年份:
    2017
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
SHF: SMALL: NONSTANDARD COMPUTATIONAL MODELS OF LINEAR LOGIC
SHF:小:线性逻辑的非标准计算模型
  • 批准号:
    1421193
  • 财政年份:
    2014
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
CCF: Medium: Validating Program Transformations in a Mechanized LLVM
CCF:中:在机械化 LLVM 中验证程序转换
  • 批准号:
    1065166
  • 财政年份:
    2011
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
TC: Small: WATCHDOG: Hardware-Assisted Prevention of All Use-After-Free Security Vulnerabilities
TC:小:WATCHDOG:硬件辅助预防所有释放后使用安全漏洞
  • 批准号:
    1116682
  • 财政年份:
    2011
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
SHF: SMALL: Practical Linear Types for Safe Protocols
SHF:SMALL:用于安全协议的实用线性类型
  • 批准号:
    1017027
  • 财政年份:
    2010
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
Unifying Events and Threads: Language Support for Network Services
统一事件和线程:网络服务的语言支持
  • 批准号:
    0541040
  • 财政年份:
    2006
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
CT-T: Resource-Guided Implementation of Secure Embedded Software
CT-T:安全嵌入式软件的资源引导实施
  • 批准号:
    0524059
  • 财政年份:
    2005
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
Collaborative Research: CT-T: Flexible, Decentralized Information-flow Control for Dynamic Environments
合作研究:CT-T:动态环境下灵活、分散的信息流控制
  • 批准号:
    0524035
  • 财政年份:
    2005
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant

相似国自然基金

胆固醇羟化酶CH25H非酶活依赖性促进乙型肝炎病毒蛋白Core及Pre-core降解的分子机制研究
  • 批准号:
    82371765
  • 批准年份:
    2023
  • 资助金额:
    50 万元
  • 项目类别:
    面上项目
锕系元素5f-in-core的GTH赝势和基组的开发
  • 批准号:
    22303037
  • 批准年份:
    2023
  • 资助金额:
    30 万元
  • 项目类别:
    青年科学基金项目
基于合成致死策略搭建Core-matched前药共组装体克服肿瘤耐药的机制研究
  • 批准号:
  • 批准年份:
    2022
  • 资助金额:
    52 万元
  • 项目类别:
鼠伤寒沙门氏菌LPS core经由CD209/SphK1促进树突状细胞迁移加重炎症性肠病的机制研究
  • 批准号:
  • 批准年份:
    2022
  • 资助金额:
    30 万元
  • 项目类别:
    青年科学基金项目
肌营养不良蛋白聚糖Core M3型甘露糖肽的精确制备及功能探索
  • 批准号:
    92053110
  • 批准年份:
    2020
  • 资助金额:
    70.0 万元
  • 项目类别:
    重大研究计划
Core-1-O型聚糖黏蛋白缺陷诱导胃炎发生并介导慢性胃炎向胃癌转化的分子机制研究
  • 批准号:
    81902805
  • 批准年份:
    2019
  • 资助金额:
    20.5 万元
  • 项目类别:
    青年科学基金项目
原始地球增生晚期的Core-merging大碰撞事件:地核增生、核幔平衡与核幔边界结构的新认识
  • 批准号:
    41973063
  • 批准年份:
    2019
  • 资助金额:
    65.0 万元
  • 项目类别:
    面上项目
CORDEX-CORE区域气候模拟与预估研讨会
  • 批准号:
    41981240365
  • 批准年份:
    2019
  • 资助金额:
    1.5 万元
  • 项目类别:
    国际(地区)合作与交流项目
RBM38通过协助Pol-ε结合、招募core调控HBV复制
  • 批准号:
    31900138
  • 批准年份:
    2019
  • 资助金额:
    24.0 万元
  • 项目类别:
    青年科学基金项目

相似海外基金

Collaborative Research: SaTC: CORE: Medium: Using Intelligent Conversational Agents to Empower Adolescents to be Resilient Against Cybergrooming
合作研究:SaTC:核心:中:使用智能会话代理使青少年能够抵御网络诱骗
  • 批准号:
    2330940
  • 财政年份:
    2024
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
Collaborative Research: SaTC: CORE: Medium: Differentially Private SQL with flexible privacy modeling, machine-checked system design, and accuracy optimization
协作研究:SaTC:核心:中:具有灵活隐私建模、机器检查系统设计和准确性优化的差异化私有 SQL
  • 批准号:
    2317232
  • 财政年份:
    2024
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
Collaborative Research: SaTC: CORE: Medium: Differentially Private SQL with flexible privacy modeling, machine-checked system design, and accuracy optimization
协作研究:SaTC:核心:中:具有灵活隐私建模、机器检查系统设计和准确性优化的差异化私有 SQL
  • 批准号:
    2317233
  • 财政年份:
    2024
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
SaTC: CORE: Medium: Increasing user autonomy and advertiser and platform responsibility in online advertising
SaTC:核心:中:增加在线广告中的用户自主权以及广告商和平台责任
  • 批准号:
    2318290
  • 财政年份:
    2024
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
SaTC: CORE: Medium: Testing the causal influence of social media on well-being and animosity
SaTC:核心:中:测试社交媒体对幸福感和敌意的因果影响
  • 批准号:
    2334148
  • 财政年份:
    2024
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
Collaborative Research: SaTC: CORE: Medium: Using Intelligent Conversational Agents to Empower Adolescents to be Resilient Against Cybergrooming
合作研究:SaTC:核心:中:使用智能会话代理使青少年能够抵御网络诱骗
  • 批准号:
    2330941
  • 财政年份:
    2024
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
SaTC: CORE: Medium: Collaborative: Hardening Off-the-Shelf Software Against Side Channel Attacks
SaTC:核心:媒介:协作:强化现成软件以抵御侧通道攻击
  • 批准号:
    2425665
  • 财政年份:
    2024
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
Collaborative Research: SaTC: CORE: Medium: Understanding the Impact of Privacy Interventions on the Online Publishing Ecosystem
协作研究:SaTC:核心:媒介:了解隐私干预对在线出版生态系统的影响
  • 批准号:
    2237329
  • 财政年份:
    2023
  • 资助金额:
    $ 120万
  • 项目类别:
    Standard Grant
Collaborative Research: SaTC: CORE: Medium: Securing Interactions between Driver and Vehicle Using Batteries
合作研究:SaTC:核心:中:使用电池确保驾驶员和车辆之间的交互安全
  • 批准号:
    2245224
  • 财政年份:
    2023
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
Collaborative Research: SaTC: CORE: Medium: Understanding and Combatting Impersonation Attacks and Data Leakage in Online Advertising
协作研究:SaTC:核心:媒介:理解和打击在线广告中的冒充攻击和数据泄露
  • 批准号:
    2247516
  • 财政年份:
    2023
  • 资助金额:
    $ 120万
  • 项目类别:
    Continuing Grant
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了