Type-based gradual enforcement of security policies for concurrent programs

顺序编程不再足以挖掘当今计算系统的全部潜力。它们需要并发编程模型，因为它们包含多核处理器并定期访问联网的分布式服务。具有基于通道通信的消息传递并发性是这些系统的一种很有前途的编程范例。作为并发的分布式程序，不能孤立地考虑，执行访问控制和保证数据完整性和机密性是至关重要的。然而，这类程序的复杂性使得声明和执行一致的安全策略具有挑战性。这个项目的总体目标是建立一个框架，用于在具有消息传递并发性的面向对象程序上声明和执行用户可配置的安全策略。该框架集中了访问控制和信息流的关注点，并依赖于静态和动态分析来执行各自的策略。它还支持逐步将安全策略引入到现有代码库中。该框架将基于会话类型和契约指定的分层策略，对应于角色层次结构。考虑的策略范围从简单的安全属性到管理安全信息流的非干扰断言。将分级策略编译成阶段监控并有效实现是该框架的核心组成部分。将通过基于浏览器的JavaScript语言实现来演示实际的适用性。

Sequential programming is no longer adequate to tap the full potential of today’s computing systems. They require concurrent programming models because they contain multi-core processors and regularly access networked, distributed services. Message-passing concurrency with channel-based communication is a promising programming paradigm for these systems.As concurrent, distributed programs cannot be considered in isolation, enforcing access control and guaranteeing data integrity and confidentiality is of utmost importance. However, the complexity of such programs makes the statement and enforcement of consistent security policies challenging.The overall goal of this project is to establish a framework for stating and enforcing user-configurable security policies on object-oriented programs with messagepassing concurrency. This framework centralizes the concerns for access control and information flow and relies on static and dynamic analysis to enforce the respective policies. It also supports the gradual introduction of security policies into an existing code base.The framework will be based on hierarchical policies specified by session types and contracts, corresponding to a role hierarchy. The policies considered range from simple safety properties to noninterference assertions that manage secure information flow. The compilation of hierarchical policies into staged monitoring and its efficient realization is a central component of the framework. Practical applicability will be demonstrated with a browser-based implementation for the JavaScript language.