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

点击翻译按钮获取中文摘要

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.