Formally Generating Adaptive Security Protocols

Over the five years of the project Formally Generating Adaptive Security Protocols, new formal tools based on original theoretical results of the research team allowed them to formally specify requirements for distributed protocols in a formal logic of system events. The project developed a constructive protocol description language and tools to automatically synthesize executable code from such descriptions and prove that the synthesized code satisfied formal requirements. These new automated tools produce many provably equivalent variants of the specified protocols that meet the requirements. The variants are used to change protocols on the fly to functionally equivalent protocols that have different behaviors. This ability to correctly change code on the fly creates a moving target defense that renders system more resistant to attack. This synthetic diversity defense was tested against attack scenarios that caused processes to fail, and the test system showed it was able to survive these attack scenarios.