As one team member explained last year, “Proving theorems about programs has been a dream of computer science for the last 60 years or more, and we’re finally able to do this at the scale required for an important, widely deployed security-critical piece of software.” And it is not just Big Tech. Microsoft has also stood up its own dedicated team on formal verification. Facebook has shown how formal verification techniques can be integrated into a “move fast and break things” approach with its INFER system, which continuously verifies the code in every update for its mobile applications. Amazon Web Services (AWS), arguably one of the most important infrastructure providers on the planet, has an entire team that uses formal methods to create “ provable security” for its customers. Leading technology companies have quietly rolled out formal methods in their core businesses. But research into formal methods continued, led by a dedicated corps of experts in academia, federal research institutions, and a handful of specialized companies. As the National Institute of Standards and Technology explains, formal methods “developed a reputation as taking far too long, in machine time, person years and project time, and requiring a PhD in computer science and mathematics to use them.” For a long time, formal methods were relegated to mission-critical use cases, such as nuclear weaponry or automotive systems, where designers were willing to devote immense time and resources to creating error free software. As software became more complicated, applying the more advanced tools for proving code-the ones that could provide the highest assurance that security vulnerabilities were absent-became exponentially more difficult. Like the neural networks that revolutionized artificial intelligence, formal methods are a technology undergoing a renaissance after spending decades in the shadows.
0 kommentar(er)
