Collaborative Research: SHF: Small: Lightweight Modular Typestate

合作研究：SHF：小型：轻量级模块化类型状态

• 批准号: 2007024
• 负责人: Manu Sridharan
• 金额: $ 25万
• 依托单位: University of California-Riverside
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-08-01 至 2024-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2007024&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Small; Lightweight

Software reliability is of critical importance to society, and software verifiers can improve reliability by guaranteeing the absence of certain bugs. In particular, typestate verification prevents important classes of bugs by ensuring programs do not perform certain illegal operation sequences. However, despite over 30 years of research, typestate verification has not been widely adopted by developers. This project will develop techniques for lightweight typestate verification, leveraging new insights on the structure of typestate properties and common programming patterns. The project is expected to make typestate verification significantly easier for programmers to adopt, thereby improving the reliability of large-scale, real-world software systems.A key barrier to adoption of typestate analysis is handling of pointer aliasing, which in extant approaches necessitates either an expensive whole-program analysis or, in modular approaches, heavyweight code annotations. This project will achieve lightweight and modular typestate verification by developing algorithms that leverage typestate system characteristics and common aliasing patterns in modern code bases. For example, the project identifies accumulation typestate systems, in which an object's enabled methods only grow over time. An accumulation typestate system can be verified soundly even in the absence of alias information. The project also studies restricted aliasing patterns arising from modern coding patterns like fluent APIs, which can be precisely analyzed with lightweight, modular techniques. The project will apply these insights both to traditional typestate systems and to new properties that are inconvenient or impossible to express in existing typestate formalisms.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.

软件可靠性对社会至关重要，软件验证者可以通过保证不存在某些错误来提高可靠性。 特别是，类型状态验证通过确保程序不执行某些非法操作序列来防止重要类别的错误。 然而，尽管经过 30 多年的研究，类型状态验证尚未被开发人员广泛采用。 该项目将开发轻量级类型状态验证技术，利用对类型状态属性结构和常见编程模式的新见解。 该项目预计将使程序员更容易采用类型状态验证，从而提高大规模、现实世界软件系统的可靠性。采用类型状态分析的一个关键障碍是处理指针别名，在现有的方法中，这需要要么昂贵的整个程序分析，或者在模块化方法中，重量级代码注释。 该项目将通过开发利用现代代码库中的类型状态系统特征和常见别名模式的算法来实现轻量级和模块化的类型状态验证。 例如，该项目识别累积类型状态系统，其中对象的启用方法仅随着时间的推移而增长。即使在没有别名信息的情况下，累积类型状态系统也可以得到良好的验证。该项目还研究由现代编码模式（例如流畅的 API）产生的受限别名模式，可以使用轻量级模块化技术对其进行精确分析。 该项目将把这些见解应用于传统的类型状态系统以及在现有类型状态形式中不方便或不可能表达的新属性。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响进行评估，被认为值得支持审查标准。

项目成果

Demanded abstract interpretation

要求抽象解释

• DOI: 10.1145/3453483.3454044
• 发表时间: 2021
• 期刊: Programming Language Design and Implementation
• 作者: Stein, Benno;Chang, Bor-Yuh Evan;Sridharan, Manu
• 通讯作者: Sridharan, Manu

Automatic Root Cause Quantification for Missing Edges in JavaScript Call Graphs

JavaScript 调用图中缺失边的自动根本原因量化

• DOI: 10.4230/lipics.ecoop.2022.3
• 发表时间: 2022
• 期刊: 36th European Conference on Object-Oriented Programming (ECOOP 2022
• 作者: Chakraborty, Madhurima;Olivares, Renzo;Sridharan, Manu;Hassanshahi, Behnaz
• 通讯作者: Hassanshahi, Behnaz

LiveDroid: identifying and preserving mobile app state in volatile runtime environments

LiveDroid：在不稳定的运行时环境中识别和保留移动应用程序状态

• DOI: 10.1145/3428228
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Farooq, Umar;Zhao, Zhijia;Sridharan, Manu;Neamtiu, Iulian
• 通讯作者: Neamtiu, Iulian

Lightweight and modular resource leak verification

• DOI: 10.1145/3468264.3468576
• 发表时间: 2021-08
• 期刊: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Martin Kellogg;Narges Shadab;Manu Sridharan;Michael D. Ernst

Verifying Object Construction

• DOI: 10.1145/3377811.3380341
• 发表时间: 2020-06
• 期刊: 2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE)
• 作者: Martin Kellogg;Manli Ran;Manu Sridharan;Martin Schäf;Michael D. Ernst