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.