Composing High-Assurance Software with the Evidential Tool Bus

ABSTRACT

The versatility and flexibility of software makes it an indispensable tool for building critical systems, but its inherent complexity opens up vulnerabilities that can compromise safety and security. High-assurance software systems must be designed with rigorous claims supported by reliable and reproducible evidence and efficient arguments that magnify the salience of potential flaws and weaknesses. We describe the Evidential Tool Bus (ETB) architecture (developed jointly with fortiss GmbH) for integrating evidence-generating tools within a design workflow for building and maintaining assurance arguments. 

BIO

Natarajan Shankar, Ph.D., is a staff scientist in the Computer Science Laboratory at SRI International. He performs research and is published across a wide spectrum ranging from fundamental mathematics to system software building. He co-developed a number of widely used tools including the highly influential Prototype Verification System (PVS) - a benchmark system for the development of proofs and the verification of algorithms against which other systems are compared - as well as SAL, Yices, Probabilistic Consistency Engine, Occam, Arsenal, and the Evidential Tool Bus. Shankar’s current research ranges from foundational aspects of logic and programming to practical applications in software development, as well as system certification.

He is also very active in the software technology community and has hosted dozens of students, professors, and technology leaders from around the world. He is PI of the DARPA SafeDocs project Parsley and DARPA ARCOS project DesCert, and co-PI of the DARPA project OPS-5G. Shankar is considered one of the leading scientists in his field, and has played a central role in several international research initiatives. 

Shankar was named an SRI Fellow in 2009.