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

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

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.