KEYNOTE: Take a SEAT: Security-Enhancing Architectural Transformations

Download
pdf

Presented as part of the 2020 HCSS conference. 

System architecture models in a language such as AADL provide a high-level setting in which existing implementations, new design features, high-level requirements, and verifications can be combined. We have recently been developing selected architecture-to-architecture transformations as a way to enhance the security of a system. The transformations are formally specified at a high level and mapped to implementations by a sequence of correctness-preserving (and deductively justified) compilation steps. We will present details of two transformations: one that creates efficient network message filters from regular expressions, and one that creates runtime monitors from temporal logic specifications. For both transformations, we illustrate an automated, end-to-end, verification path that formally connects top-level component specifications with the binary behavior of the newly introduced security gadgets. Since these gadgets are expected to run in an embedded system, further properties, such as execution time and liveness, are required, and we will discuss how our framework can prove those as well. Time permitting, we will also discuss aspects of how this formal toolchain is incorporated into a build system which maps AADL architecture models to system images in seL4 and Linux.

Dr. Konrad Slind (PhD TU Munich) is a Senior Industrial Logician in the Trusted Systems Group of Collins Aerospace. He has been at Collins Aerospace for ten years; previous stints were at University of Utah School of Computing (faculty), Cambridge University Computer Lab, and Bell Labs. Slind's main area of research is the design, implementation, and application of interactive theorem provers. He has published on a variety of verification topics, including hardware verification, compiler verification, and block cipher verification. At Collins, he is currently working on the DARPA CASE project.

Tags:
License: CC-2.5
Submitted by Anonymous on