Compositional Testing of Network Protocols for Attacks
Abstract
The proposed work is to use light-weight formal methods so to detect and analyze security vulnerabilities of Internet protocols. Finding such vulnerabilities is often accomplished by exploring specific attacks on specific implementations. The work described here offers a novel methodology that will allow to detect attacks even at the specification level of protocols, thus the framework may help detect vulnerability that are common to all implementations of the same protocol. In addition, the methodology will allow to generalize from an attack on one implementation onto an attack on all other implementations of the same protocol The approach builds on prior work of the PI that constructed a methodology for compositional testing of Internet protocols against their formal specification. Using and expanding on this methodology, the proposed work will construct formal models of attackers which will be composed with the system under test. Combining advanced techniques from disciplines such as formal methods, program debugging, machine learning, and neural network , attack traces will be used to generate attack strategies and included in a family of attacker models. The work will be implemented on the new Internet transport protocol QUIC, introduced by Google, and currently in the process of IETF standardization. QUIC is intended to replace the TLS/TCP stack and guarantee communication that is secure, authenticated, and ordered. It is also designed to provide improved performance in various areas, including initial latency, handling of multiple streams, data loss detection and congestion control, and resistance to denial of service attacks. Currently, variants of the protocol are estimated to carry above 5% of traffic on the Internet. It is currently being implemented by several of the major generators of traffic, including Google, Apple and Microsoft, and will be the transport protocol for the next version of HTTP, called HTTP/3. The results of the work will be reported to the developers of QUIC implementations and to the IETF. The project will offer research opportunity to numerous students at all of BSc, MSc, and PhD levels.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Aug 31, 2020
- Source ID
- W911NF2010310
Entities
People
- Lenore Zuck
Organizations
- Army Contracting Command
- Office of the Secretary of Defense
- University of Illinois at Chicago