Model-driven Synthesis of High Assurance Secure Systems
Abstract: Programming languages research has many techniques for generating efficient, correct implementations from high-level specifications. Recent research on language-based security formulates models of information security in terms of modular, algebraic structures from language semantics. The research described in this talk combines these threads in novel ways to construct high-assurance secure systems in which semantic techniques from programming languages research provide both a mathematical basis for formal verification and a flexible, modular organizing principle for system design and implementation. This methodology is currently being applied in the MU High Assurance Security Kernel Lab to a significant case study in which secure kernels (in this case, separation kernels) with a verified security policy are synthesized from formal models of security rooted in language semantics.
Bio: Dr William Harrison received his BA in Mathematics from Berkeley in 1986 and his doctorate from the University of Illinois at Urbana-Champaign in 2001 in Computer Science. From 2000-2003, he was a post-doctoral research associate at the Oregon Graduate Institute in Portland, Oregon where he was a member of the Programatica project. Dr Harrison has been an assistant professor in Computer Science at the University of Missouri since 2003 and received the NSF CAREER award from the CyberTrust program in December of 2007. His research interests include language-based computer security and software verification.
