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多年，但开发人员尚未广泛采用prokestate验证。 该项目将开发用于轻量级访问验证的技术，利用对打字属性和常见编程模式结构的新见解。 预计该项目将使程序员更容易采用典型验证，从而提高了大型现实世界软件系统的可靠性。采用类型分析的关键障碍是处理指针别名，在现存的方法中，这种方法需要一种昂贵的全面编程分析，或者在模块化的方法中，重量级的量子，重量级的代码注释。 该项目将通过开发利用典型的系统特征和现代代码库中常见的混叠模式的算法来实现轻质和模块化典型验证。 例如，该项目标识累积型典型系统，其中对象的启用方法只会随着时间的推移而增长。即使没有别名信息，也可以很好地验证累积型系统。该项目还研究了由现代编码模式（如Fluent 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

Accumulation Analysis

• DOI: 10.4230/lipics.ecoop.2022.10
• 发表时间: 2022
• 作者: 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