SPARK in Formal Verification Research

Kansas State University, Manhattan, Kansas (US)

Prof. John Hatcliff and his team at Kansas State University’s Static Analysis and Transformation of Software (SAnToS) Laboratory have found the SPARK language technology to be an ideal research vehicle for exploring novel techniques in formal program verification. The SAnToS team has worked for over a decade on innovative tools that incorporate model checking, symbolic execution, data flow, and program dependence analyses. “We started out using Java”, said Prof. Hatcliff. “But Java is a large language with complex semantics, and it certainly wasn’t designed for, or often used in, safety-critical systems. It was hard for us to produce clean technical results and robust tools with Java, and to apply those tools to interesting safety-critical examples. SPARK has proved to be a much more appropriate base language.”

Inspired by challenges they observed while collaborating with Rockwell Collins engineers on certified embedded information assurance applications, and with US Food and Drug Administration engineers on next generation medical devices, SAnToS researchers are working on several innovative enhancements to SPARK’s annotations for software contracts:

  • Precise information flow specification and checking. Embedded information assurance components such as crypto-graphical controllers and cross domain solutions often have information flow policies that are conditional (i.e., data can flow from one domain to another only under certain conditions). This requires specifying how information flows through individual cells or ranges of elements in complex data structures built using arrays and records. SAnToS researchers are extending SPARK’s derives annotations to support declaration of conditional flows and precise descriptions of flows through arrays.

  • Highly automated checking of complex pre/postconditions. Checking complex pre/postconditions in SPARK can require significant manual interactions with SPARK’s Proof Checker. SAnToS researchers have developed an alternate tool chain based on symbolic execution that can perform bounded checking of such contracts in a completely automated fashion, and can automatically generate unit test cases representing the paths explored in the analysis.

SAnToS researchers are currently working with AdaCore and Altran Praxis to include some of these functionalities in the upcoming SPARK 2012 framework. For more information, please visit the website.