CAREER: Automated Synthesis of High-Assurance Security Kernels

编程语言研究有许多技术可以从高级规范生成高效、正确的实现。近年来，基于语言的安全研究从语言语义出发，以模块化、代数结构的方式构建信息安全模型。本研究以新颖的方式结合这些线程来构建高保证的安全系统，其中编程语言语义技术为形式验证提供了数学基础，并为系统设计和实现提供了灵活的模块化组织原则。通过一个案例研究说明了这种方法，在这个案例研究中，具有经过验证的安全策略的内核（特别是分离内核）是直接从正式的安全模型合成的。国防和航空电子领域对分离内核越来越感兴趣，作为一种处理因使用高水平集成而引起的对系统安全、安全和完整性的严重关切的手段。多级安全（MLS）系统可以通过物理隔离实现：不同安全级别的计算位于不同的网络节点上。然而，对于许多国防和航空电子场景，由于资源紧张，物理分离是不可行的。由于共享资源会引入潜在的漏洞，因此任务或安全关键型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.