DeepMind Uses AI Tool to Formally Verify Signal Protocol Security

According to WIRED, Google DeepMind researchers used a new AI framework called AlphaProof Code to formally verify that the Signal protocol operates as intended within four weeks. The analysis did not find new vulnerabilities in the protocol portions examined, but correctly identified issues in an older version of Signal containing known legacy vulnerabilities and showed that the protocol failed formal verification. DeepMind research scientist Swarat Chaudhuri said this is a milestone in extending formal verification to all software worldwide, though there is still a long way to go. The researchers also published the specifications and proofs developed for this analysis to assist other formal verification efforts.

Source: TechFlow