CT-ISG: Attacker Models and Verification Methods for End-to-End Protocol Security

社会越来越依赖互联网信息流，缺乏适当的安全是一个普遍的威胁。 目前的技术往往侧重于特定组件的安全性;但最终需要的是端到端的安全保证，以保护整个系统免受非常广泛的潜在类型的攻击。 这项研究正在开发新的技术，重写逻辑的公共语义框架的基础上，获得高保证的端到端的安全性的协议系统组成的不同组件的整体系统架构。 将包括不同的系统方面和安全问题，例如：（一）保密性和真实性保证;（二）防止拒绝服务攻击;（三）图形用户界面可被破坏的网络浏览器系统;和（iv）与整个系统架构相关的紧急系统范围漏洞。在许多个人和组织之间传输重要数据信息依赖于协议-其端到端安全性经常受到损害的中介服务。 预计拟议的研究将为在未来系统中实现更高的端到端安全保证提供基础，并对端到端安全标准的制定产生潜在影响。 该项目还寻求通过课程开发、研究生和本科生研究培训、促进更广泛的参与以及能够提高普通受众认识的公开讲座来产生重大的教育影响。

Society relies ever more heavily on the Internet flow of information and the lack of proper security is a pervasive threat. Current techniques tend to focus on the security of specific components; but what are ultimately needed are end-to-end security guarantees protecting an entire system against a very broad range of potential types of attacks. This research is developing new techniques, based on the common semantic framework of rewriting logic, to gain high assurance about the end-to-end security of protocol systems made up of different components within an overall system architecture. Different system aspects and security concerns will be included such as: (i) confidentiality and authenticity guarantees; (ii) preventing denial of service (DoS) attacks, and (iii) web browser systems whose graphical user interface (GUI) can be subverted; and (iv) emergent system-wide vulnerabilities associated with overall system architecture.Transmission of vital data information across many individuals and organizations relies on protocol-mediated services whose end-to-end security is routinely compromised. The proposed research is expected to provide a basis for achieving much higher end-to-end security assurance in future systems and to have potential impact on the development of standards for end-to-end security. The project also seeks substantial educational impact through course development, graduate and undergraduate research training, promotion of broader participation, and public lectures that can raise awareness for general audiences.