Collaborative Research: SHF: Medium: Ensuring Safety and Liveness of Modern Systems through Dynamic Temporal Analysis

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

• 批准号: 2107169
• 负责人: Eric Koskinen
• 金额: $ 40万
• 依托单位: Stevens Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-07-15 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2107169&HistoricalAwards=false
• 关键词: Collaborative; Research; 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 应用程序和服务器、实时视频流软件和物联网平台等反应/交互系统已深深嵌入现代世界的各个方面。人们已经创建了许多程序分析技术和工具来分析这些系统的重要时间属性，这些属性涵盖安全性（“不会发生任何坏事”）和活跃性（“最终会发生好事”）。不幸的是，现代静态分析在处理许多实际应用程序中经常出现的复杂程序语义方面仍然受到限制：它们仅支持简单的属性，产生误报，或者无法扩展到大型程序。最近的动态或“数据驱动”方法解决了静态分析的几个缺点，可以更有效地分析更复杂的程序属性，但有时会产生不正确的结果。该项目的新颖之处在于静态和动态方法的理论和实践整合，用于分析、定位和修复反应/交互式系统的时间方面。该项目的影响是新理论和算法的发展，产生了确保当今反应式/交互式软件的安全性/活性的先进方法。当今的软件涉及复杂的非线性行为、堆操作和高阶功能。该项目使用动态分析可以推断这些程序的表达属性，而使用静态验证可以验证这些推断的属性。此外，静态验证和动态学习相互告知并增强彼此的力量，允许进行安全性/活性分析，甚至可以进行故障定位和对暂时缺陷的修复综合。正在开发的方法体现在越来越多的公开发布的自动化工具中。研究结果用于开发新课程、高级设计项目以及编程语言和软件工程方面的交互式 Jupyter 书籍。该项目通过多项举措扩大参与范围，针对调查人员所在社区中代表性不足的群体的中/高中学生和本科生。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

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

Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

用于时间验证的模块化原对偶定点逻辑求解

• DOI: 10.1145/3571265
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Unno, Hiroshi;Terauchi, Tachio;Gu, Yu;Koskinen, Eric
• 通讯作者: Koskinen, Eric