CAREER: Realizing Practical High Assurance through Security-Typed Information Flow Systems

帕特里克麦克丹尼尔宾夕法尼亚州立大学CAREER：通过安全类型的信息流系统实现实用的高保证0643907小组ID：070111摘要该基金支持正式的模型，算法，方法，工具和基础设施的调查，建立在安全类型的语言的信息流保证，以实现高保证软件系统。 安全类型语言的信息流保证提供了一个切实可行的途径来实现系统的安全性，通过生产的实现的遵守一个指定的政策的证据。 然而，这些语言仅仅是通过源代码注释来限制信息流的工具：它们没有提供理论或实践来说明如何使用这些注释来实现真实的系统中的安全性。 这项工作弥合了系统安全和安全类型语言之间的理论和实践差距。 在这方面，以下三个中心研究重点正在调查中：a）通过模型和算法将高级策略映射到安全的实现，这些模型和算法能够生成语义等效的策略，并自动解释代码来执行这些策略，B）研究管理应用程序和基础设施信息流的服务和语言，以及c）探索用信息流政策来规范遗留系统的工具。 示范性的独立、分布式和多用户应用程序和系统正在开发中，并在广泛的安全目标方面得到评估。 评估工作包括追求正确性的形式证明和性能和安全权衡的实证分析。

Patrick McDanielPennsylvania State UniversitycAREER: Realizing Practical High Assurance through Security-Typed Information Flow Systems0643907Panel ID:070111AbstractThis grant supports an investigation of formal models, algorithms,methods, tools, and infrastructure that build upon the informationflow guarantees of security-typed languages to achieve high assurancesoftware systems. The information flow guarantees of security-typedlanguages provide a practical avenue to achieving system security byproducing proofs of an implementation's compliance with a specifiedpolicy. However, these languages are simply tools for restrictinginformation flow through source-code annotations: they provide notheory or practice to indicate how such annotations can be used toimplement security in real systems. This work bridges the theoreticaland practical gap between systems security and security-typedlanguages. In this, the following three central research thrusts areunder investigation: a) the mapping of high-level policies to secureimplementations through models and algorithms that enable thegeneration of semantically equivalent policies and the automatedinstrumentation of code to enforce them, b) the study of services andlanguages that govern application and infrastructure information flow,and c) the exploration of tools to instrument legacy systems withinformation flow policy. Demonstrative stand-alone, distributed, andmulti-user applications and systems are being be developed andevaluated with respect to a broad range of security goals. Theevaluation efforts include pursing formal proofs of correctness andempirical analysis of performance and security tradeoffs.