VeriWeird: Formal Verification of Weird Networks
Leader of the formal verification (FA2) research area of the VeriWeird project. VeriWeird’s key innovation is to develop a novel approach to the formalzation of hidden communication systems (HCS) that is based on the encoding of (HCS) properties in the simulation-based cryptgraphy proof paradigm.
The goal of simulation-based cryptography is to establish probabilistic indistinguishability between an ideal world, where the primitive is secure by definition, and the real world, where concrete protocols are executed. In terms of HCS, the real world represents the execution of the HCS channel (like Balboa) and the ideal world represents the application channel (like WebRTC) on top of which the HCS channel of the real world is defined. The ideal world can then use a simulator whose goal is to generate a plausible execution trace of the application channel that matches the real-world traces from the HCS channel. If the traces produced by the real world are indistinguishable from those produced by the ideal world, the protocol is secure since security is built into the definition of the ideal world. Because the blocking of HCSs is based on detecting discrepancies between traces generated by its execution and the ideal-world application, our simulation-based approach provides an apposite proof paradigm.