CT-ISG: An Architecture and Policies for Secure Network-facing Applications

几乎无处不在的互联网接入将丰富的信息和不断增加的社交互动机会置于用户的指尖。推动这场革命的是现代网络浏览器，它已经从一个旨在显示静态数据的相对简单的客户端应用程序演变为一个复杂的网络操作系统，负责管理用户在线体验的许多方面。对动态内容、多媒体数据和第三方插件的支持极大地丰富了用户体验，但却增加了浏览器本身的复杂性。因此，当前的Web浏览器充满了安全漏洞，为黑客提供了通过基于浏览器的攻击轻松访问最终用户系统的机会。到目前为止，浏览器安全努力基本上是对现有网络浏览器的改进，只取得了有限的成功，因为现代网络浏览器的设计存在根本缺陷。为了解决这个问题的根源，这项研究将为任何面向网络的用户应用程序开发一种本质上更安全的设计方法，并将通过设计和实现名为OP的新的安全Web浏览器来验证这一方法。总体设计方法将操作系统社区的分离和安全原则与正式方法社区开发的验证和监控技术结合在一起。通过将浏览器划分为较小的子系统，并使子系统之间的所有通信简单而明确，这项研究工作可以利用这两个社区的技术来获得有关OP的正确性和限制受危害子系统影响的能力的正式保证。

The near ubiquity of Internet access has put a wealth of information and ever-increasing opportunities for social interaction at the fingertips of users. Driving this revolution is the modern web browser, which has evolved from a relatively simple client application designed to display static data into a complex networked operating system tasked with managing many facets of a users online experience. Support for dynamic content, multimedia data, and third-party plug-ins has greatly enriched users experiences at the cost of increasing the complexity of the browser itself. As a result, current web browsers are plagued with security vulnerabilities that provide hackers with easy access to end-user systems via browser-based attacks. Browser security efforts to date are essentially retrofits for existing web browsers and have enjoyed only limited success, as the design of modern web browsers is fundamentally flawed. To address the root of this problem, this research will develop an inherently more secure design methodology for any network-facing user application, which will be validated through the design and implementation of a new secure web browser called OP. The overall design approach combines separation and safety principles from the operating system community with validation and monitoring techniques developed by the formal methods community. By partitioning the browser into smaller subsystems and making all communication between subsystems simple and explicit, this research effort can leverage techniques from both of these communities to elicit formal guarantees about OP's correctness and ability to limit the effects of compromised subsystems.