SHF: Small: Scalable and Maximal Predictive Runtime Verification for Concurrent Software

多核处理器的计算能力只有通过并发软件才能释放，随着多核处理器的日益广泛使用，使得软件缺陷或错误变得更加常见，检测和修复变得更加劳动密集型。运行时验证是一种新的分析方法，它从运行的系统中提取信息，并使用这些信息来检测并可能对满足或违反某些属性的观察到的行为做出反应。运行时验证具有良好的伸缩性，避免了传统形式验证技术的复杂性。该项目开发的技术将通过提供一种可扩展的替代正式验证的方法来产生健壮的产品质量软件，该方法为安全和安全提供许多相同的保证。该项目旨在为并发软件开发可扩展的预测性运行时验证框架。与现有技术相比的一个主要技术进步是，它不仅在运行时检测错误，而且能够在实际出现之前预测一般的安全和安全属性违规行为，通过采取用户定义的适当操作来防止不良行为的发生。这个项目建立在一个合理的最大因果模型的基础上，从而在没有虚假警报的情况下，对观察到的痕迹提供了可证明的最大可能的预测能力。这项工作的核心研究见解是探索并发与自动约束求解之间的最大因果关系，这一问题已经研究了几十年，并正在变得越来越强大。

The increasingly widespread use of multicore processors, whose computing powercan only be unleashed by concurrent software, makes software defects, or bugs,become more common and labor-intensive to detect and repair. Runtime verificationis a novel analysis approach that extracts information from a running system anduses it to detect and possibly react to observed behaviors satisfying or violatingcertain properties. Runtime verification scales well and avoids the complexity oftraditional formal verification techniques. The techniques developed in this project will lead to robust production quality software by providing a scalable alternative to formal verification that provides many of the same guarantees for safety and security.This project aims to develop a scalable predictive runtime verification frameworkfor concurrent software. A major technical advancement over prior art is that itnot only detects errors when they occur at runtime, but is able to predict generalsecurity and safety property violations before they actually surface, preventingbad behaviors from happening by taking proper actions defined by the users. Thisproject builds upon a sound and maximal causal model, hereby providing the provablymaximum possible prediction power on the observed trace with no false alarms. Thecore research insight of this work is to explore the maximal causality of concurrencywith automated constraint solving, which has been studied for decades and is becomingincreasingly powerful.