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

社会越来越依赖互联网信息流，缺乏适当的安全保障是一个普遍存在的威胁。当前的技术倾向于关注特定组件的安全性；但最终需要的是端到端安全保证，保护整个系统免受各种潜在类型的攻击。本研究旨在开发基于重写逻辑的通用语义框架的新技术，以获得对整个系统架构中由不同组件组成的协议系统的端到端安全性的高保证。不同的系统方面和安全问题将包括在内，例如：(i)保密和真实性保证；（ii）防止拒绝服务（DoS）攻击，以及（iii）图形用户界面（GUI）可被破坏的web浏览器系统；（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.