Composing High-Assurance Software
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 motivate the need for constructing software hand-in-hand with an assurance argument supporting the critical safety and security claims. We describe some technologies that we have been developing to assist with design for assurance. Specifically, we outline the “efficient argument” approach to system design, the use of formal architectures as a foundation for efficient compositional arguments, ontic type analysis linking the requirements ontology to code-level representations, automatic code generation from high-level specifications, and the Evidential Tool Bus (ETB) architecture for integrating evidence-generating tools within a design workflow for building and maintaining assurance arguments.
Dr. Natarajan Shankar is a Distinguished Senior Scientist and SRI Fellow at the SRI Computer Science Laboratory. He received a B.Tech. degree in Electrical Engineering from the Indian Institute of Technology, Madras, and a Ph.D. in Computer Science from the University of Texas at Austin. He is a co-recipient of the 2012 CAV Award and the recipient of the 2022 CADE Herbrand Award.