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

几乎无处不在的互联网接入为用户的指尖提供了丰富的信息和不断增加的社会互动机会。推动这场革命的是现代web浏览器，它已经从一个设计用于显示静态数据的相对简单的客户机应用程序演变为一个复杂的网络操作系统，其任务是管理用户在线体验的许多方面。对动态内容、多媒体数据和第三方插件的支持极大地丰富了用户体验，但代价是增加了浏览器本身的复杂性。因此，当前的web浏览器受到安全漏洞的困扰，这些漏洞使黑客可以通过基于浏览器的攻击轻松访问最终用户系统。迄今为止，浏览器安全方面的努力基本上是对现有web浏览器的改进，而且只取得了有限的成功，因为现代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.