Collaborative Resaerch: SHF: Medium: Ensuring Safety and Liveness of Modern Systems through Dynamic Temporal Analysiss

协作研究：SHF：中：通过动态时间分析确保现代系统的安全性和活力

• 批准号: 2106845
• 负责人: Timoleon Antonopoulos
• 金额: $ 40万
• 依托单位: Yale University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-07-15 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2106845&HistoricalAwards=false
• 关键词: Collaborative; Resaerch; SHF; Medium; Ensuring

Reactive/interactive systems such as web applications and servers, real-time video streaming software, and IoT platforms are deeply embedded into all aspects of the modern world. Many program-analysis techniques and tools have been created to analyze important temporal properties of these systems that span both safety ("nothing bad will happen") and liveness ("something good eventually happens"). Unfortunately, modern static analyses are still limited in handling complex program semantics that often appear in many real-world applications: they support only simple properties, produce false positives, or do not scale to large programs. Recent dynamic or "data-driven" approaches address several shortcomings of static analyses to analyze more complex program properties more efficiently, yet sometimes yield incorrect results. The project's novelties are the theoretical and practical integration of static and dynamic approaches to analyze, localize, and repair temporal aspects of reactive/interactive systems. The project's impacts are the development of new theories and algorithms, giving rise to advanced methods for ensuring the safety/liveness of today's reactive/interactive software.Today's software involves complex non-linear behavior, heap manipulations, and higher-order features. The project's use of dynamic analysis enables inference of expressive properties of these programs, while the use of static verification allows for validation of those inferred properties. Furthermore, static verification and dynamic learning mutually inform and bolster the power of each other, allowing for safety/liveness analyses, and even for the localization of faults and synthesis of repairs for temporal defects. The methods being developed are embodied in a growing collection of automated tools to be released publicly. The results of the research are used to develop new courses, senior design projects, and an interactive Jupyter book in programming languages and software engineering. The project broadens participation through several initiatives, aimed at middle/high school students and undergraduate students from underrepresented groups in the investigators' local communities.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应用程序和服务器、实时视频流软件和物联网平台等反应式/交互式系统深深嵌入到现代世界的各个方面。许多程序分析技术和工具已经被创建来分析这些系统的重要时间属性，这些属性涵盖了安全性（“不会发生任何坏事”）和活跃性（“最终会发生一些好事”）。不幸的是，现代静态分析在处理复杂的程序语义方面仍然受到限制，这些语义经常出现在许多现实世界的应用程序中：它们只支持简单的属性，产生误报，或者不能扩展到大型程序。最近的动态或“数据驱动”的方法解决了静态分析的几个缺点，以更有效地分析更复杂的程序属性，但有时会产生不正确的结果。该项目的新颖之处是静态和动态方法的理论和实践整合，以分析，本地化和修复反应/交互系统的时间方面。该项目的影响是新的理论和算法的发展，从而产生了先进的方法，以确保今天的反应/交互式软件的安全性/活性。今天的软件涉及复杂的非线性行为，堆操作和高阶特征。该项目的动态分析的使用，使这些程序的表达属性的推断，而静态验证的使用允许验证这些推断的属性。此外，静态验证和动态学习相互通知和支持彼此的力量，允许安全/活性分析，甚至用于故障的定位和临时缺陷的修复的合成。正在开发的方法体现在越来越多的公开发布的自动化工具中。研究结果用于开发新课程，高级设计项目，以及编程语言和软件工程的交互式电子书。该项目通过多项举措扩大了参与范围，目标群体是研究者所在社区中代表性不足的初中/高中学生和本科生。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Analyzing Intentional Behavior in Autonomous Agents under Uncertainty

分析不确定性下自主主体的意图行为

• DOI: 10.24963/ijcai.2023/42
• 发表时间: 2023
• 期刊: International Joint Conferences on Artificial Intelligence Organization
• 作者: Cano Córdoba, Filip;Judson, Samuel;Antonopoulos, Timos;Bjørner, Katrine;Shoemaker, Nicholas;Shapiro, Scott J.;Piskac, Ruzica;Könighofer, Bettina
• 通讯作者: Könighofer, Bettina

ppSAT: Towards Two-Party Private SAT Solving

ppSAT：迈向两方私人 SAT 解决方案

• 发表时间: 2022
• 期刊: USENIX
• 作者: Luo, N;Judson, S;Antonopoulos, T;Piskac, R;Wang, X
• 通讯作者: Wang, X

Proving UNSAT in Zero Knowledge

零知识证明 UNSAT

• DOI: 10.1145/3548606.3559373
• 发表时间: 2022
• 期刊: ACM conference on Computer and Communications Security
• 作者: Luo, Ning;Antonopoulos, Timos;Harris, William R.;Piskac, Ruzica;Tromer, Eran;Wang, Xiao
• 通讯作者: Wang, Xiao

An Algebra of Alignment for Relational Verification

关系验证的对齐代数

• DOI: 10.1145/3571213
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Antonopoulos, Timos;Koskinen, Eric;Le, Ton Chanh;Nagasamudram, Ramana;Naumann, David A.;Ngo, Minh
• 通讯作者: Ngo, Minh

Representing Regular Languages of Infinite Words Using Mod 2 Multiplicity Automata

使用 Mod 2 多重自动机表示无限字的正则语言

• DOI: 10.1007/978-3-030-99253-8
• 发表时间: 2022
• 期刊: Foundations of Software Science and Computation Structures
• 作者: Angluin, Dana;Antonopoulos, Timos;Fisman, Dana;George, Nevin
• 通讯作者: George, Nevin