CAREER: Automated Synthesis of High-Assurance Security Kernels

编程语言研究有许多技术可以从高级规范生成高效、正确的实现。最近对基于语言的安全的研究从语言语义出发，用模块化的代数结构来建立信息安全模型。本研究以新颖的方式将这些线索结合在一起，以构建高保证的安全系统，其中来自编程语言语义的技术为形式化验证提供了数学基础，并为系统设计和实现提供了灵活的、模块化的组织原则。通过一个案例研究说明了这种方法，其中具有经过验证的安全策略的内核(特别是分离内核)是直接从安全的形式模型合成的。国防和航空电子界对分离内核越来越感兴趣，将其作为一种手段，以应对由于使用高度集成而引起的对系统安全性、安全性和完整性的严重担忧。多级安全系统可以通过物理分离来实现：不同安全级别的计算位于不同的网络节点上。然而，对于许多国防和航空电子设备场景，由于严格的资源限制，物理分离是不可行的。由于共享资源会带来潜在的漏洞，因此任务关键型或安全关键型MLS系统既需要高度集成的实现，也需要高保证的安全保证。这项研究将对分离内核的设计、实现和验证产生直接影响。构建模块化和健壮的安全系统的严格技术可以推广到其他系统吗？长期目标是促进具有高保证端到端保证的系统的构建，从而使高保证更广泛地可用。

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. This research combines these threads in novel ways to construct high-assurance secure systems in which techniques from programming language semantics provide both a mathematical basis for formal verification and a flexible, modular organizing principle for system design and implementation. This methodology is illustrated with a case study in which kernels (in particular, separation kernels) with a verified security policy are synthesized directly from formal models of security. There is growing interest within defense and avionics circles in separation kernels as a means of coping with serious concerns for system security, safety and integrity arising from the use of high levels of integration. Multi-level security (MLS) systems can be implemented by physical separation: computations at different security levels are situated on different network nodes. However, for many defense and avionics scenarios, physical separation is infeasible due to tight resource constraints. Because sharing resources introduces potential vulnerabilities, mission- or safety-critical MLS systems require both highly integrated implementations and high-assurance security guarantees. This research will have a direct impact on how separation kernels are designed, implemented and verified. Can the rigorous techniques for constructing modular and robust secure systems be generalized to other systems? The long range goal is to facilitate the construction of systems with high assurance end-to-end guarantees, thereby making high assurance more widely available.