Buterin: AI Can Verify Program Security, Not Just Critical Components

Vitalik Buterin, co-founder of Ethereum, is pushing back against concerns that AI-powered hacking will make cybersecurity increasingly difficult. In a recent post, he disagreed with the idea that AI hacking means 'cybersecurity is doomed.'

Buterin believes that modern AI could allow developers to verify entire programs instead of just checking security-critical parts. He gave an example involving advanced artificial intelligence and mathematics: if AI can prove complex mathematical theorems like Navier-Stokes and FLT, it should be able to prove a program's security as well.

However, Buterin emphasized that defining what 'secure' means is much harder than it sounds. A system can have many different security concerns that need to be considered, including how an attacker might interfere with the system, information leakage, and hardware or software failure.

To address these issues, Buterin advocates for making security definitions more human-readable and using better tools to verify whether a program satisfies those definitions. He sees an advantage in working with definitions, which are additive and can be combined to prove that a program satisfies multiple definitions at once.