Formal Verification in Cloud Computing Security

Making use of regularity, a common feature of all distributed protocols, could potentially automate the formal verification process of the Paxos protocol, theoretically enabling software and hardware to be released with substantially less testing, argues a University of Michigan study.  

The Lamport’s Paxos Consensus protocol, a highly complex algorithm that enabled the rise of cloud computing and blockchain applications, had always been presumed as too convoluted for automated security verification, thereby requiring hours on manual oversight.

“There have been many attempts in the past to verify Paxos, including many manual attempts,” study architect, Aman Goel said. “Everyone points to a prior theoretical result that says automating it is impossible—it is beyond the tools of automation to be able to prove it.”

Instead of assessing the algorithm as a single monolith, the two doctoral researchers proposed breaking down the large momentous task into manageable batches under the premise of regularity, which refers to server processing of large batches of requests that are intrinsically the same, but differ only slightly over time. In practice this required verifying the protocol under the assumption that it had a fixed number of nodes and then generalizing the solution to a “theoretically unbounded number.”

The checking system tool, called IC3PO, looks through every state a program can enter and determines whether it corresponds with the established parameters of safe behavior. If the protocol is deemed “correct” an inductive invariant is produced, a proof demonstrating that the property holds in all cases. Inversely, if a protocol bug is found, the tool will produce a counter-example and execution trace, showing step-by-step how the bug manifests.

This apparently foolproof formal verification system tool not only gives a certificate of correctness but also cuts the manhours dedicated to identifying system failures. Insofar, this process stands to expedite and revolutionize software and hardware development with assurance that when deployed they will function as intended. As cloud computing comes front in center in multiple sectors, taking on increasingly weighted processes, the application of this tool could potentially mitigate the occurrence of server outages, hacking incidents and buggy network behavior.

This stands to be a highly valuable protocol for emerging economies like Mexico, which are under an accelerated digitalization process that has often left gaps that hackers have attempted to exploit.