SHF: Small: Inferring Specifications for Blackbox Code

SHF：小：推断黑盒代码规范

• 批准号: 1910769
• 负责人: Osbert Bastani
• 金额: $ 50万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-10-01 至 2023-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1910769&HistoricalAwards=false
• 关键词: SHF; Small; Inferring; Specifications; Blackbox

Writing error-free computer software is notoriously difficult. Yet, software errors (bugs) can have catastrophic consequences, ranging from loss of user data and security vulnerabilities to loss of property and even loss of life. Thus, designing tools that help software developers identify and fix bugs is of critical importance. The goal of this project is to contribute to the development of these kinds of tools. In particular, a key challenge faced by all such tools is the need for specifications that describe the properties of software libraries shared among many applications. Often, without these specifications, the library code cannot be analyzed, substantially diminishing the usefulness of bug-finding tools. This project's novelty lies in the development of algorithms that use machine learning to automatically infer these kinds of specifications. The project outcomes will substantially improve the usefulness of bug-finding tools, thereby reducing the number of bugs in software.As a part of this project, the researchers design novel and general algorithms for inferring specifications for blackbox code (i.e., code that can be executed but not instrumented or analyzed). Focusing on the blackbox setting ensures that the algorithms will work in a broad range of settings, ranging from native code to code only available over a network connection. These algorithms infer specifications by executing the code on carefully chosen inputs, observing the corresponding output, and then generalizing the observed behaviors to specifications. Furthermore, to improve performance, these algorithms use reinforcement-learning to automatically learn domain-specific search strategies, eliminating the need for end users to manually design heuristic search strategies for their problem domain.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.

编写无错误的计算机软件是出了名的困难。然而，软件错误（bug）可能会造成灾难性的后果，从用户数据丢失和安全漏洞到财产损失甚至生命损失。因此，设计帮助软件开发人员识别和修复错误的工具至关重要。该项目的目标是促进这类工具的开发。特别是，所有这些工具面临的一个关键挑战是需要规范，描述许多应用程序之间共享的软件库的属性。通常，如果没有这些规范，库代码就不能被分析，从而大大降低了缺陷查找工具的有用性。该项目的新奇在于使用机器学习来自动推断这些规格的算法的开发。该项目的成果将大大提高缺陷发现工具的实用性，从而减少软件中的缺陷数量。作为该项目的一部分，研究人员设计了新颖的通用算法来推断黑盒代码的规范（即，可以被执行但不能被插装或分析的代码）。专注于黑盒设置可以确保算法在广泛的设置中工作，从本机代码到仅通过网络连接可用的代码。这些算法通过在精心选择的输入上执行代码，观察相应的输出，然后将观察到的行为概括为规范来推断规范。此外，为了提高性能，这些算法使用启发式学习来自动学习特定领域的搜索策略，从而消除了最终用户手动为其问题领域设计启发式搜索策略的需要。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Synthesizing Programmatic Policies that Inductively Generalize

• 发表时间: 2020-04
• 期刊: ArXiv
• 作者: J. Inala;O. Bastani;Zenna Tavares;Armando Solar-Lezama

Counterfactual Explanations for Natural Language Interfaces

自然语言界面的反事实解释

• 发表时间: 2022
• 期刊: Annual Meeting of the Association for Computational Linguistics
• 作者: Tolkachev, George;Mell, Stephen;Zdancewic, Stevve;Bastani, Osbert
• 通讯作者: Bastani, Osbert

Offline Goal-Conditioned Reinforcement Learning via f-Advantage Regression

通过 f-Advantage 回归进行离线目标条件强化学习

• 发表时间: 2022
• 期刊: Advances in neural information processing systems
• 作者: Ma, Yecheng Jason;Yan, Jason;Jayaraman, Dinesh;Bastani, Osbert
• 通讯作者: Bastani, Osbert

Generating Programmatic Referring Expressions via Program Synthesis

通过程序合成生成程序引用表达式

• 发表时间: 2020
• 期刊: International conference on machine learning
• 作者: Huang, Jiani;Smith, Calvin;Bastani, Osbert;Singh, Rishabh;Albarghouthi, Aws;Naik, Mayur
• 通讯作者: Naik, Mayur

PAC Prediction Sets Under Covariate Shift

• 发表时间: 2021-06
• 期刊: ArXiv
• 作者: Sangdon Park;Edgar Dobriban;Insup Lee;O. Bastani