abstract:

Software-dependent critical systems that impact daily life are rapidly increasing in number, size, and complexity. Unfortunately, inadequate software and systems engineering can lead to accidents that cause economic disaster, injuries, or even death. There is a growing reliance on development and verification tools to reduce costs, better manage complexity, and to increase confidence in these systems. Recent standards for critical systems have an increased emphasis on characterizing the requirements of tools used in the certification context and the particular certification obligations that these tools can discharge. In the case of avionics, DO-333 explicitly addresses the role/use of formal methods tools, e.g., allowing formal verification of code compliance to procedure contracts to complement unit testing, and DO-330 addresses tool qualifications.

In this talk, I will present the Kiasan symbolic execution framework that can be used to automatically check varying degrees of functional correctness properties of critical systems — ranging from absence of runtime errors to compositional reasoning of deep semantical contracts of complex data structures. One notable feature of Kiasan is the focus on explicating its analysis results to describe inconclusive analysis results in cases where it cannot clearly refute or verify properties. Similar to other symbolic execution tools, Kiasan generates counter-examples or test cases as evidence for (conclusive) contract violations. In contrast to others, however, Kiasan can generate strong evidence for its (conclusive) verification results in the form of Coq proof objects. This is achieved by first formalizing Kiasan’s symbolic execution (abstract) semantics in Coq and proving that it is sound and relatively complete with respect to the (concrete) semantics of the system programming language; this is done once and for all (for a particular system programming language) and establishes a relatively small trust base. We believe that Kiasan’s evidence-based trust approach can be used to help in software certifications of safety-critical systems as well as in tool qualification processes.

bio:

Robby is a Professor in the Computing and Information Sciences (CIS) Department at Kansas State University. In addition to symbolic execution-based verification, he works on dataflow framework for analyzing security vulnerability in mobile apps, device modeling for interoperable medical devices, and a hazard analysis platform. In the past, he worked on software model checking, data/predicate abstractions, program dependences (slicing), and software specification techniques.