|
CS Home
Dept Info/Contacts
People
Research
Events
Courses
Undergrad Programs:
Computer Science
Informatics
Graduate Program
Prospective Students
Faculty Hiring
Employment
Resources
Help Lab Hours
Student Groups
Support the Department: Weeg Professorship
|
|
Model-driven Synthesis of High Assurance Secure Systems
Friday, Oct 23, 2009
4:00-5:00pm, 140 SH (Schaeffer Hall)
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.
|
