By 
On November 3, the Defense Advanced Research Projects Agency (DARPA) issued an Artificial Intelligence Exploration (AIE) Opportunity inviting submissions of innovative basic or applied research concepts in the technical domain of Formal Methods. Responses are due by 4:00 p.m. Eastern on December 2.
The Proof Engineering, Adaptation, Repair, and Learning for Software (PEARLS) Opportunity aims to explore the use of AI and machine learning (ML) to support and, if possible, automate the generation and maintenance of proofs used in the formal verification of software.
There is growing interest in adopting formal proofs to provide assurance for software, as there have been successful deployments of proof tools in the Department of Defense (DoD) and industrial practice, providing a level of assurance not possible through testing alone. However, such analysis has been hampered by the limited size and complexity of problems that can be addressed, and the highly specialized skills needed to exercise formal verification tools.
As a result, the ability to objectively determine that software contains no flaws, with respect to a specification, is very limited. Moreover, any attempt to update or maintain the software can invalidate a formal proof, requiring significant effort to repair the proofs. Most current research has focused on the problem of proof design – how to set up a formal artifact alongside code so as to assure desirable properties. But all engineered systems change over time, and at this point breakages are inevitable. Common changes that will often invalidate the proofs created during formal verification include (1) the code may change (e.g., a patch is pushed to continuous integration); (2) the environment may change (e.g., the operating system is updated, or a new nuance of the system is discovered such as an architectural side channel); or (3) the proof may change (e.g., a theorem may be refactored or the verification tool is updated to a new version).
The PEARLS AIE seeks novel methods of developing formal proofs that can be trained on limited data in order to significantly improve formal proof construction, evolution, or repair. For example, a method such as transfer learning techniques could learn patterns for a particular code DARPA-PA-21-04-04 change in one context and update the change for application in a different proof context, or generative techniques, such as generative adversarial networks (GANs), may be able to create proof elements much more rapidly and effectively than current heuristic approaches.
As scalable proof repair techniques are developed, proofs would be integrated into the normal software development process with the need for formal methods expertise being limited to just the most difficult cases. Then existing proof technologies could be applied in many more software engineering contexts in support of critical DoD national security systems with the effort of maintaining a proof being comparable to the effort of maintaining the software. Moderate code changes would result in moderate – and automated – proof repairs.
Usability is also a key aim in this workflow, with two key technical enablers. First, the verification tool should present salient, actionable information to the engineer to make decisions. Second, proof information, when accessed by the engineer, should be presented in a manner that is intuitive to a journeyman developer who is not a specialist in formal methods. Rather than perform a complete repair of the proof, the repair should focus on just the aspects of the proof relevant to the changes. Both locality and compositionality are critical elements of a more usable proof tool.
Review the full DARPA PEARLS AIE.
Source: SAM
IC News brings you business opportunities like this one each week. If you find value in our work, please consider supporting IC News with a subscription.
