INFDok - Dokumentenvolltextserver des Fachbereichs Informatik

Kurzfassung auf Englisch:

Modern communication fundamentally relies on the security of cryptographic protocols. However, even if a protocols design is formally proven secure, its implementation may still be vulnerable. While many tools exist to verify either protocol specifications or general software correctness independently, there is a lack of methods for directly comparing existing implementations against formal protocol models. This thesis investigates the feasibility of automating such a comparison and proposes how a tool capable of analyzing both protocol implementations and specifications should be designed. This includes identifying functional and non-functional requirements and recommendations for the tool and for the input languages, determining which specifications and implementation languages to support, and finally assessing suitable software correctness methods to implement the comparison. To this end, this thesis reviews formal software correctness methods, including dynamic analysis, static analysis, and machine learning approaches, along with their classifications and representative tools. It then identifies essential requirements for an automatic comparison tool, focusing on widely used input languages, correctness guarantees, and scalable methods. To determine which protocol specifications are commonly used in practice, an extensive literature review of protocol verification tools is conducted. The identified requirements are subsequently used to provide design consideration, assess which input languages should be supported, and which software correctness techniques are best suited to implement the tool. This also includes analyzing the constraints of the selected methods on the protocol implementations. Static analysis methods, such as abstract interpretation, deductive verification, bounded model checking, and symbolic execution, best fulfill the requirements and are among the most suitable approaches. However, these methods typically require a substantial amount of manual annotation, often expressed as assertions and assumptions in the form of function contracts. Moreover, they differ significantly from practical protocol specification languages, such as the applied pi calculus and the Alice & Bob notation. Therefore, formal methods should be complemented by machine learning techniques to enable the automatic translation of verified protocol specifications into software correctness annotations. Thus, this thesis provides design considerations for achieving such an automatic comparison, focusing on applicability, correctness, and scalability.