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

Patrick McDaniel宾夕法尼亚州立大学cAREER：通过安全类型的信息流系统实现实用的高保证小组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.