Many years ago, I worked with some colleagues on an ill-fated topic: we tried to write down a logical statement concerning the guarantees provided by atomic multicast systems that manage their own membership. Today, we know how to do that, courtesy of Lamport’s Paxos specification and the proof methods he introduced.
But those were the Wild West days, and that particular project occurred before the Paxos specification was created. Moreover, our atomic multicast (which actually could be configured as a Paxos protocol), also included some optional features Leslie omitted from Paxos, for good reason. Those centered on a form of optimistic early delivery combined with barrier synchronization (analogous to a memory fence).
Our puzzle centered on expressions describing "all the possible" future behaviors that could arise with this rather complex optimistic form of early delivery. The problem was that the set of future scenarios grew exponentially as new members join and existing members failed (or exited voluntarily). Our logic needed to "account" for all of these possibilities. In fact, the logic itself had a flaw, but even had we managed to write it down properly, we still would have had a semantic in which statements can only be interpreted within the “space” of future scenarios. Since it is intractable to do model checking in an exponentially growing state space, such statements are often undecideable: they can have a true or false value and yet no decision procedure can be created that will terminate in bounded time.
A total mess. We ultimately abandoned the effort, tails between our legs, and came to view it as an embarrassment. The less said about it, the better!
Except... I sometimes tell the story, as a cautionary tale.
Not every technology suffers from the issue we encountered. Lamport's way of formalizing Paxos avoids the issue by avoiding speculative "early delivery", which was the real issue in our early work. This is one reason that Lamport's Paxos specification was such a success.
Transactional database models also have a better way of handling such problems: when we ask whether a database system is in a serializable state, the rule is to start by erasing all the uncommitted transactions, at which point serializability is defined as a property of the committed state. This approach accepts that transactions could glimpse inconsistent states while executing: it isn't a problem so long as those transactions can't commit. Moreover, it erases all the events that depend on future outcomes, neatly avoiding the whole issue our unfortunate effort ran up against.
Which brings us to BlockChain. I'm intrigued by the recent work that seeks to put a kind of transactional database behavior "into" the BlockChain, by incorporating SQL-like statements into the transactions themselves, but then reevaluating them as the BlockChain steadily grows.
To appreciate why this poses the same problem I struggled with twenty years ago, think about a smart contract that says something along the following lines: "John agrees to sell me his horse, Bucky, for the sum of $1,500, and has accepted a $150 deposit. If I haven't completed the purchase within a week, John agrees to return the deposit. But in the meanwhile, John can continue to try and sell Bucky. If he finds another buyer, he can cancel my transaction, but in that case must both return the deposit and also pay me an addition $100, to compensate me for my trouble."
The world is full of contracts like these. Smart contracts can express things like rules for computing interest that depend on global interest rates. We probably all remember 2008, when the world financial system melted down over issues with mortgage-backed securities split into interest and principle. The claim is that the expressive power of smart contracts is a good thing, because smart contracts can be analyzed by tools (compiler-style tools), and hence it should be possible to automatically identify risks. Risk managers would then have robust ways to compute their risk and hedge against it, and those hedging contracts (insurance deals) could also be carefully evaluated, etc. Back in 2008, it wasn't the mortgage-backed securities that collapsed, per-se. It was the insurance companies that insured them, but didn't hedge the "secondary" risk properly.
So... how does one attach a "formal meaning" to a smart contract? Let's go back to John's sale of Bucky. Notice that this contract depends on how things play out into the future. For the coming week, the BlockChain will grow, and each new block added to the chain could bring events relevant to the contract. John could decide to cancel the contract and sign a new contract with Sally (perhaps she is ready to pay more -- enough to more than compensate John for the $100 he'll forfeit). I could show up with the remaining $1350, and head home with Bucky. A week could pass, and John would have to return my $150 deposit. And it gets worse: John could sign with Sally, but then Sally might cancel her deal, and perhaps John would then want to reinstate his deal with me.
Much as in that early work I tried to do, John's smart contract with me has a meaning that can depend on a branching future state: some large (maybe exponential) space of possibilities, each leading to its own proper interpretation of the correct "thing to do". Should John hand Bucky over to me, or not? Do I owe him $1,350, or does he owe me $150, or should it be $250?
Without much trouble, we can design sequences of smart contracts in which to know the proper outcome for my contract, I need to figure out the outcome of Sally's contract (and this then becomes an induction, because Sally's contract may depend on the outcome of Carl's contract). This is precisely how my early work failed: you end up with scenarios that can be arbitrarily prolonged, and the total space of scenarios grows exponentially in the length of the future chain, because of an endlessly longer sequence of new events that each depends on its own future outcomes.
Beyond all of which we have the issue of rollbacks: even if you accept the common wisdom and adopt the view that a BlockChain prefix has magically "committed" once it has been extended by six or more blocks, we still run into the problem that the suffix is unstable. So we could have one suffix in which Sally's transaction finalizes, but it might then rollback, aborting that outcome and perhaps replacing it with one in which Sally cancels her purchase.
Should it trouble us that smart contracts on BlockChains might not have a tractable meaning -- a reduction to temporal logic -- if they include future references? For that matter, even without future references, some of the aspects just mentioned would still arise. Is this bad?
I think so: it seems to me that in computing, if we're learned one thing over the decades, it is the overarching importance of rigorous semantics. If BlockChains with smart contracts can't be reduced to a stable logical framework in which proofs can be carried out without solving infeasible problems (evaluating logical formulas within exponentially growing state spaces is a well-known infeasible problem), then we are looking at a profoundly untrustworthy framework.
So beware, all of you rabid BlockChain investors! If you are betting big on smart contracts, you owe it to yourselves to figure out a way to reduce the statements those contracts make to a stable, computationally feasible form. You know what they say: those who fail to learn from the past are doomed to repeat it. If you don't find a robust and tractable semantics for your technology, then someday, twenty years from you, too will be writing little blog postings about how your work once took a hopelessly wrong turn... and that Professor Birman's sad story of his unfortunate foray into the theory of branching future executions should have warned you!
Showing posts with label formal methods. Show all posts
Showing posts with label formal methods. Show all posts
Tuesday, 25 September 2018
Thursday, 9 August 2018
Magical Thinking and the Logical Foundations of BlockChains
During the past few years, I've been exposed to an unrelenting drumbeat for BlockChains. The level of enthusiasm for this model, and the commercial mania around it, have all the elements of a "market bubble". Just yesterday I saw a quote from a BlockChain/CyberCoin billionaire who believes that "BlockChain will replace the Internet." Really? But search for that phrase and you'll actually find that this guy is saying something many people believe. Rational or not, there is a huge community totally convinced that the future will be a giant BlockChain.
The BlockChain buzz was evident at the recent conference I attended, where one speaker told us about a Berkeley spin-off based on BlockChain: Oasis, which just landed $45M in first-round "seed" funding. Just think about that for a moment: how can such a number be justified? I'm a skeptic.
Oasis apparently plans to build a secure infrastructure using BlockChain as the storage solution, but entirely secure from the ground up. Presumably this is one reason Oasis needed so much cash: most companies these days just run on a public cloud like Azure or Amazon (or any of the others). Building from the ground up will be expensive, but would let Oasis avoid a pitfall other startups share: because its competitors depend on existing datacenters, they are exposed to whatever security flaws those cloud platforms embody.
But can one build a secure data center from the ground up? Let's focus purely on storage, since this seems to be the essence of the Oasis plan. Could one build a new kind of secure data center that (only) provides secure storage using BlockChain, built from the ground up?
The first step is to reject the permissionless BlockChain model, which is too weak to guarantee freedom from rollbacks even years after a transaction seemingly commits: permissionless BlockChain systems with anonymous servers are insecure by design. We want a minimal BlockChain solution, but if you take minimal to mean "anonymous, globally replicated, permissionless", my answer is that "it can't be done: it is impossible to create a trustworthy platform with that mix of properties and technologies."
Fortunately, the permissioned model avoids this risk. Moreover, it seems reasonable to assume that if the goal is to offer a data-center BlockChain product, the data center operator can control which machines can operate the solution. This moves us from the BitCoin style of anonymous, amorphic, fully decentralized BlockChain to a more standard model of append-only files used by customers like banks.
Next, we should perhaps reject a standard cloud that offers encrypted append-only files. This is an interesting step in the analysis because a block chain really is just a secure append-only file, no matter what anyone might tell you (secured using SHA 256 hashes or similar block hashes, with proof-of-work if the system is permissionless, and then with the signatures entangled to prevent tampering). Any file system could play that role, if you code the needed logic to generate records formatted this way and with the required chain of attestation. Amazon and Azure and other cloud companies already offer extremely secure storage layers, including BlockChain services. But as noted, they do depend on other elements of the respective datacenter systems. So out with the old, and in with the new!
Now, without knowing anything about the proprietary protocols that Oasis is presumably designing, I can't say anything about how they plan to guarantee correctness. But I can tell you how I would do it. I would use a form of Paxos, and because I would want extreme speed, would go with the version of durable Paxos that we implemented in Cornell's Derecho system. If I were chief architect at Oasis, I might want to build my own software (hence not use Derecho), but I would certainly adopt the Paxos specification, and prove that my software implements it.
Of course being a Derecho zealot, I'm going to make the case that using Derecho might be the smart move, even if you might have preferred to roll your own.
First, I should note that by using Paxos, Derecho is able to leverage decades of work on proofs of correctness -- Derecho was implemented by fusing a proved-correct version of Paxos integrated with a proved-correct version of the virtual synchrony membership management model and a new reliable (but not atomic) multicast layer. Then all of the data movement steps were mapped to the available storage (SSD or 3-D XPoint) and communications technologies (RDMA or TCP) in an efficient way. Finally, Derecho uses specialized optimizations for code paths that turn out to be performance-critical.
Next, it is worth noting that Derecho is open source, hence can benefit from community contributions over time, and also that the system is extremely fast -- the fast such system ever created. Further, it actually achieves minimal bounds for Paxos (Derecho's protocols are "optimal" in a formal sense). Of course one can talk about smaller constants and so forth, but given the speed of the system, there is an obvious case to be made that the constants aren't showing any sign of being unreasonably large. So Derecho is a genuinely interesting option! Heck, maybe my students and I should try and raise $50M or so and jump into the commercial space!
But now we run into the first of a series of issues: the protocols and proofs we are leveraging were all created in the usual way: on paper, by hand. The mapping didn't modify the underlying logic, yet it required to adapt them to modern networking is by hand, too, and hence also needed to be proved by hand. The same can be said about our dozens of optimizations.
Is there really a sensible way to argue that all of these hand-written proofs be accepted as somehow being "more trustworthy" than Amazon AWS or Azure? After all, those are companies are serious about specifications too, and further, both have invested hundreds of millions of dollars in their testing and Q/A process. Derecho is remarkably robust, and we would point to all those proofs as part of the reason, but even so, we do find bugs in our logic.
Now, if I had the money, one option might be to harden Derecho. Aggressive testing, deep quality assurance and better documentation would be a breeze. Starting with such a strong prototype, we could quickly end up with a professional-quality tool. In fact I actually hope to do this, in the next year or so, if Derecho users are able to chip in to help with the costs.
But perhaps you still wouldn't be satisfied. And indeed, today's state of the art goes much further: the very best approach is to only run code extracted from a machine-checked proof. In effect, we compile the proof into the running system and take the developers entirely off the development path.
This, though, turns out to be infeasible for software as elaborate as Derecho, and would be even harder for whatever Oasis really plans to build. The issue here is that as of today, the provers can't handle the style of code that we needed to use in order to create Derecho, and any full data-center infrastructure would have 10x more such code, and perhaps far more than just 10x.
Today's best provers actually can handle automated extraction of Paxos code from correctness proofs (this has been done using NuPRL here at Cornell, or IOA and Larch in Nancy Lynch's group at MIT, or IronFleet, using Dafny at Microsoft). The resulting solutions are very robust in the sense that the logical proof structures that result are rock solid -- for what they cover. Unfortunately, however, the resulting code is incredibly slow compared to Derecho. Moreover, infrastructure aspects are much harder to formalize than data replication and consistency, so in some sense, Paxos is the "easy" part of the story. Can we specify the system, fully? Is the specification itself bullet-proof? Bootstrap? Other management tasks? These steps are much harder than many people would expect. They may not even be possible, in some cases!
This same pattern is evident in many projects that have formalized aspects of operating systems or runtime environments. At MIT, Nick Zeldovich famously proved a very simple file system correct a few years ago. It ran on Linux, but there is a Linux u-kernel called SEL4 that has been proved correct, and while it doesn't cover all of Linux, SEL4 probably has enough stuff in it to support Nick's provably correct file system.
Then you could perhaps use the proved version of the C compiler to compile the thing (C++ is considered to be too complex for existing provers). Even better would be to just build the whole thing in a language like RUST or Dafny, where proof is much more central to the coding and compilation model. With such help, you may actually manage to create a proved solution, for parts of your full system.
But without exception, you'll end up with slow code compared to the best possible, and will have solved just a portion of the entire datacenter infrastructure. We are decades from having data-center scale, provably correct , ultra-performant software systems. Perhaps we'll never get there.
Moreover, even if we did manage to overcome these barriers, we would run into further questions.
One big issue is the hardware. Think about any hardware component in the entire data center. The routers. Printers. Digital telephone systems. Storage devices.
$45M may seem like a huge amount of money, but in fact it is a tiny drop in the bucket when you consider that companies like Intel spend billions on their VLSI chip fabrication factories. So there is simply no question that Oasis will end up using components some other company created.
The problem is that these components tend to be software-defined, and this is becoming more and more of a standard story: Almost all hardware components have general-purpose, highly capable processors within them. An entire separate computer, with its own memory, network interfaces and code.
Indeed, if you needed one CPU and DRAM unit just to operate the hardware, why not include two on the same board, or chip? Who would notice? And if you do this, why not drop malicious code into the second unit? Your printer company may not even realize that it is selling compromised devices: I've heard of network chips that had entire secondary networking infrastructures built in, operated by entire stealth operating systems. You can monitor your network as closely as you like. You would never notice the stealth network, and its control logic!
So you can perhaps make the higher layers provably secure, but this issue of trust in the hardware limits the degree that the resulting system could be secure.
If you run a secure solution on compromised hardware, all bets are off. The situation is a bit better if you trust the hardware: Intel has an approach called SGX that can do a bit better, and perhaps Oasis plans to leverage it, but if so, they will face performance challenges. Sadly, SGX is quite slow.
But suppose they pull all of this off: a ground-up datacenter solution, minimal trust in the hardware, offering a BlockChain storage layer to customers. Now we run into a new puzzle: the issue arises of how to draw the boundary between the trusted storage solution and the customer's application.
The problem here has to do with composing a trusted application with a trusted storage layer through some form of less-trusted layer of intermediary logic, like the runtime associated with the programming language. Modern applications are coded in standard languages like Java, Python, C++, Ruby. They use databases from big vendors like Oracle, web servers like Apache, and so forth... and each of brings its own millions of lines of logic and its own runtime environment. Those presumably have flaws, hence an attacker could potentially compromise the application by compromising some element of the compiler or runtime, even if other aspects of the datacenter BlockChain storage solution magically were iron-clad.
And this is why I'm a skeptic: I don't see how such a picture can be secured, not today, and probably not in my lifetime.
I actually do believe in security, but I think that in modern systems, we get much more protection from diversity and multiple layers of monitoring than we do from automated techniques like verification. We should definitely do verification where we can -- for systems like Derecho, it offers a path that can slash bug rates and greatly improve confidence in the correctness of the system relative to the promises it can legitimately make. But to me we oversell the power of verification and proofs if we go further and allow people to believe that we have discovered a magic way to carry this idea to the limits and "prove the whole thing", whatever that thing may be. BlockChains don't change this reality.
The Oasis folks will presumably read this blog, and I should emphasis that it isn't a personal criticism. I'm a huge fan of the Berkeley security team and have been amazed by their accomplishments. Amazing work has been done. But even so, and without being hostile in any way at all, I do think we all share a need to be frank with the public about what technology can, and cannot, accomplish.
BlockChains are being oversold as a trivial way to get perfect security -- not by Oasis, but by the popular technology press, which seems to have a very dim understanding of the concept. The press seems to think BlockChains are somehow "more" than secure file systems. Yet if anything, they are "less"!
Perhaps we are seeing a superposition of two elements. Clearly, we do have a community that was unaware of the concept of a tamper-proof append-only log protected using cryptography. All sorts of folks who work in government, health care, manufacturing clearly feel that this is a revelation, and offers an answer to all their security worries. And quite possibly some were actually not aware that we can use file systems in secure ways -- I'm glad they know, now, and if BlockChain helps them conceive of this, I'm all for it.
Then we have hype, driven by cryptocurrency valuations in the stratosphere, a technology press endlessly eager for the next big thing, and investors keen to make a killing. In this marketplace, I see a lot of value that companies can bring to the table, particularly ones with exciting ideas for packaging this stuff to be useful, and some of this value is very real: HyperLedger and Ethereum and related tools are genuinely powerful.
But just the same, we need to stop claiming that BlockChain is a revolutionary invention.
My worry is that by overselling the same old file systems to a naïve community of infrastructure owners, we may end up with systems that are actually less secure than what they replace. After all, a platform like Azure is actually remarkably secure today, managed professionally by a company obsessed with security (and nobody is paying me to say this, by the way!), and has such a diversity of technologies deployed that compromising it in a major way would be quite hard. If some hospital were to abandon that and jump to BlockChain as its file system, the illusion of security may have replaced much stronger real security. True, today's reality has its limits, but in fact I would be far more comfortable seeing medical records hosted on Azure or AWS, than abandoning these professional solutions in favor of a storage product that uses BlockChain as a magic wand to solve all problems.
But clearly, the current climate (especially the technology press) is prone to magical thinking, and a bit weak on just what BlockChains are, and how they work, and what their logical foundations turn out to be. And in light of that, I suppose that the amazingly high first round of Oasis investment makes a kind of sense. A bubble? Definitely. And yet all valuations are measures of market sentiment. So perhaps not an unreasonable bubble, given the modern business climate and the craze that BlockChain has engendered.
The BlockChain buzz was evident at the recent conference I attended, where one speaker told us about a Berkeley spin-off based on BlockChain: Oasis, which just landed $45M in first-round "seed" funding. Just think about that for a moment: how can such a number be justified? I'm a skeptic.
Oasis apparently plans to build a secure infrastructure using BlockChain as the storage solution, but entirely secure from the ground up. Presumably this is one reason Oasis needed so much cash: most companies these days just run on a public cloud like Azure or Amazon (or any of the others). Building from the ground up will be expensive, but would let Oasis avoid a pitfall other startups share: because its competitors depend on existing datacenters, they are exposed to whatever security flaws those cloud platforms embody.
But can one build a secure data center from the ground up? Let's focus purely on storage, since this seems to be the essence of the Oasis plan. Could one build a new kind of secure data center that (only) provides secure storage using BlockChain, built from the ground up?
The first step is to reject the permissionless BlockChain model, which is too weak to guarantee freedom from rollbacks even years after a transaction seemingly commits: permissionless BlockChain systems with anonymous servers are insecure by design. We want a minimal BlockChain solution, but if you take minimal to mean "anonymous, globally replicated, permissionless", my answer is that "it can't be done: it is impossible to create a trustworthy platform with that mix of properties and technologies."
Fortunately, the permissioned model avoids this risk. Moreover, it seems reasonable to assume that if the goal is to offer a data-center BlockChain product, the data center operator can control which machines can operate the solution. This moves us from the BitCoin style of anonymous, amorphic, fully decentralized BlockChain to a more standard model of append-only files used by customers like banks.
Next, we should perhaps reject a standard cloud that offers encrypted append-only files. This is an interesting step in the analysis because a block chain really is just a secure append-only file, no matter what anyone might tell you (secured using SHA 256 hashes or similar block hashes, with proof-of-work if the system is permissionless, and then with the signatures entangled to prevent tampering). Any file system could play that role, if you code the needed logic to generate records formatted this way and with the required chain of attestation. Amazon and Azure and other cloud companies already offer extremely secure storage layers, including BlockChain services. But as noted, they do depend on other elements of the respective datacenter systems. So out with the old, and in with the new!
Now, without knowing anything about the proprietary protocols that Oasis is presumably designing, I can't say anything about how they plan to guarantee correctness. But I can tell you how I would do it. I would use a form of Paxos, and because I would want extreme speed, would go with the version of durable Paxos that we implemented in Cornell's Derecho system. If I were chief architect at Oasis, I might want to build my own software (hence not use Derecho), but I would certainly adopt the Paxos specification, and prove that my software implements it.
Of course being a Derecho zealot, I'm going to make the case that using Derecho might be the smart move, even if you might have preferred to roll your own.
First, I should note that by using Paxos, Derecho is able to leverage decades of work on proofs of correctness -- Derecho was implemented by fusing a proved-correct version of Paxos integrated with a proved-correct version of the virtual synchrony membership management model and a new reliable (but not atomic) multicast layer. Then all of the data movement steps were mapped to the available storage (SSD or 3-D XPoint) and communications technologies (RDMA or TCP) in an efficient way. Finally, Derecho uses specialized optimizations for code paths that turn out to be performance-critical.
Next, it is worth noting that Derecho is open source, hence can benefit from community contributions over time, and also that the system is extremely fast -- the fast such system ever created. Further, it actually achieves minimal bounds for Paxos (Derecho's protocols are "optimal" in a formal sense). Of course one can talk about smaller constants and so forth, but given the speed of the system, there is an obvious case to be made that the constants aren't showing any sign of being unreasonably large. So Derecho is a genuinely interesting option! Heck, maybe my students and I should try and raise $50M or so and jump into the commercial space!
But now we run into the first of a series of issues: the protocols and proofs we are leveraging were all created in the usual way: on paper, by hand. The mapping didn't modify the underlying logic, yet it required to adapt them to modern networking is by hand, too, and hence also needed to be proved by hand. The same can be said about our dozens of optimizations.
Is there really a sensible way to argue that all of these hand-written proofs be accepted as somehow being "more trustworthy" than Amazon AWS or Azure? After all, those are companies are serious about specifications too, and further, both have invested hundreds of millions of dollars in their testing and Q/A process. Derecho is remarkably robust, and we would point to all those proofs as part of the reason, but even so, we do find bugs in our logic.
Now, if I had the money, one option might be to harden Derecho. Aggressive testing, deep quality assurance and better documentation would be a breeze. Starting with such a strong prototype, we could quickly end up with a professional-quality tool. In fact I actually hope to do this, in the next year or so, if Derecho users are able to chip in to help with the costs.
But perhaps you still wouldn't be satisfied. And indeed, today's state of the art goes much further: the very best approach is to only run code extracted from a machine-checked proof. In effect, we compile the proof into the running system and take the developers entirely off the development path.
This, though, turns out to be infeasible for software as elaborate as Derecho, and would be even harder for whatever Oasis really plans to build. The issue here is that as of today, the provers can't handle the style of code that we needed to use in order to create Derecho, and any full data-center infrastructure would have 10x more such code, and perhaps far more than just 10x.
Today's best provers actually can handle automated extraction of Paxos code from correctness proofs (this has been done using NuPRL here at Cornell, or IOA and Larch in Nancy Lynch's group at MIT, or IronFleet, using Dafny at Microsoft). The resulting solutions are very robust in the sense that the logical proof structures that result are rock solid -- for what they cover. Unfortunately, however, the resulting code is incredibly slow compared to Derecho. Moreover, infrastructure aspects are much harder to formalize than data replication and consistency, so in some sense, Paxos is the "easy" part of the story. Can we specify the system, fully? Is the specification itself bullet-proof? Bootstrap? Other management tasks? These steps are much harder than many people would expect. They may not even be possible, in some cases!
This same pattern is evident in many projects that have formalized aspects of operating systems or runtime environments. At MIT, Nick Zeldovich famously proved a very simple file system correct a few years ago. It ran on Linux, but there is a Linux u-kernel called SEL4 that has been proved correct, and while it doesn't cover all of Linux, SEL4 probably has enough stuff in it to support Nick's provably correct file system.
Then you could perhaps use the proved version of the C compiler to compile the thing (C++ is considered to be too complex for existing provers). Even better would be to just build the whole thing in a language like RUST or Dafny, where proof is much more central to the coding and compilation model. With such help, you may actually manage to create a proved solution, for parts of your full system.
But without exception, you'll end up with slow code compared to the best possible, and will have solved just a portion of the entire datacenter infrastructure. We are decades from having data-center scale, provably correct , ultra-performant software systems. Perhaps we'll never get there.
Moreover, even if we did manage to overcome these barriers, we would run into further questions.
One big issue is the hardware. Think about any hardware component in the entire data center. The routers. Printers. Digital telephone systems. Storage devices.
$45M may seem like a huge amount of money, but in fact it is a tiny drop in the bucket when you consider that companies like Intel spend billions on their VLSI chip fabrication factories. So there is simply no question that Oasis will end up using components some other company created.
The problem is that these components tend to be software-defined, and this is becoming more and more of a standard story: Almost all hardware components have general-purpose, highly capable processors within them. An entire separate computer, with its own memory, network interfaces and code.
Indeed, if you needed one CPU and DRAM unit just to operate the hardware, why not include two on the same board, or chip? Who would notice? And if you do this, why not drop malicious code into the second unit? Your printer company may not even realize that it is selling compromised devices: I've heard of network chips that had entire secondary networking infrastructures built in, operated by entire stealth operating systems. You can monitor your network as closely as you like. You would never notice the stealth network, and its control logic!
So you can perhaps make the higher layers provably secure, but this issue of trust in the hardware limits the degree that the resulting system could be secure.
If you run a secure solution on compromised hardware, all bets are off. The situation is a bit better if you trust the hardware: Intel has an approach called SGX that can do a bit better, and perhaps Oasis plans to leverage it, but if so, they will face performance challenges. Sadly, SGX is quite slow.
But suppose they pull all of this off: a ground-up datacenter solution, minimal trust in the hardware, offering a BlockChain storage layer to customers. Now we run into a new puzzle: the issue arises of how to draw the boundary between the trusted storage solution and the customer's application.
The problem here has to do with composing a trusted application with a trusted storage layer through some form of less-trusted layer of intermediary logic, like the runtime associated with the programming language. Modern applications are coded in standard languages like Java, Python, C++, Ruby. They use databases from big vendors like Oracle, web servers like Apache, and so forth... and each of brings its own millions of lines of logic and its own runtime environment. Those presumably have flaws, hence an attacker could potentially compromise the application by compromising some element of the compiler or runtime, even if other aspects of the datacenter BlockChain storage solution magically were iron-clad.
And this is why I'm a skeptic: I don't see how such a picture can be secured, not today, and probably not in my lifetime.
I actually do believe in security, but I think that in modern systems, we get much more protection from diversity and multiple layers of monitoring than we do from automated techniques like verification. We should definitely do verification where we can -- for systems like Derecho, it offers a path that can slash bug rates and greatly improve confidence in the correctness of the system relative to the promises it can legitimately make. But to me we oversell the power of verification and proofs if we go further and allow people to believe that we have discovered a magic way to carry this idea to the limits and "prove the whole thing", whatever that thing may be. BlockChains don't change this reality.
The Oasis folks will presumably read this blog, and I should emphasis that it isn't a personal criticism. I'm a huge fan of the Berkeley security team and have been amazed by their accomplishments. Amazing work has been done. But even so, and without being hostile in any way at all, I do think we all share a need to be frank with the public about what technology can, and cannot, accomplish.
BlockChains are being oversold as a trivial way to get perfect security -- not by Oasis, but by the popular technology press, which seems to have a very dim understanding of the concept. The press seems to think BlockChains are somehow "more" than secure file systems. Yet if anything, they are "less"!
Perhaps we are seeing a superposition of two elements. Clearly, we do have a community that was unaware of the concept of a tamper-proof append-only log protected using cryptography. All sorts of folks who work in government, health care, manufacturing clearly feel that this is a revelation, and offers an answer to all their security worries. And quite possibly some were actually not aware that we can use file systems in secure ways -- I'm glad they know, now, and if BlockChain helps them conceive of this, I'm all for it.
Then we have hype, driven by cryptocurrency valuations in the stratosphere, a technology press endlessly eager for the next big thing, and investors keen to make a killing. In this marketplace, I see a lot of value that companies can bring to the table, particularly ones with exciting ideas for packaging this stuff to be useful, and some of this value is very real: HyperLedger and Ethereum and related tools are genuinely powerful.
But just the same, we need to stop claiming that BlockChain is a revolutionary invention.
My worry is that by overselling the same old file systems to a naïve community of infrastructure owners, we may end up with systems that are actually less secure than what they replace. After all, a platform like Azure is actually remarkably secure today, managed professionally by a company obsessed with security (and nobody is paying me to say this, by the way!), and has such a diversity of technologies deployed that compromising it in a major way would be quite hard. If some hospital were to abandon that and jump to BlockChain as its file system, the illusion of security may have replaced much stronger real security. True, today's reality has its limits, but in fact I would be far more comfortable seeing medical records hosted on Azure or AWS, than abandoning these professional solutions in favor of a storage product that uses BlockChain as a magic wand to solve all problems.
But clearly, the current climate (especially the technology press) is prone to magical thinking, and a bit weak on just what BlockChains are, and how they work, and what their logical foundations turn out to be. And in light of that, I suppose that the amazingly high first round of Oasis investment makes a kind of sense. A bubble? Definitely. And yet all valuations are measures of market sentiment. So perhaps not an unreasonable bubble, given the modern business climate and the craze that BlockChain has engendered.
Monday, 18 September 2017
What we can learn about specifications from ZooKeeper's asynchronous mode, and its unsafe ForceSync=no option?
At the time of this writing, ZooKeeper is surely the world's most widely used data replication tool. You run it on a few machines, normally 3, and it offers a file system API with very strong guarantees to the user. In fact, if configured to do so, ZooKeeper implements the Paxos specification: Leslie Lamport's formalism of the properties required for correct state machine replication. (My post-doc, Weijia Song, points out that actually, the Zookeeper Atomic Broadcast, ZAB, isn't necessarily a true Paxos protocol, but the issue he raises is very subtle, so I'll set that to the side. For our purposes here, ZAB is close enough).
In a recent blog posting, we discussed some of the missing aspects of that very specification. As a result, when I read the ZooKeeper documentation, I was intrigued to realize that the documentation more or less urges that the system be configured to violate Paxos! In fact the document is short, and easy to read, so have a look if you are skeptical.
You'll learn about all sorts of parameters that represent ZooKeeper's response to those missing specification elements, such as how to deal with disks that fill up completely, or avoiding inconsistency in the list of servers running the ZooKeeper service.
And then, in the middle of the same document, you run into a fascinating option: there is a small section called "Unsafe configuration options" that explains that "The following options can be useful, but be careful when you use them. The risk of each is explained along with the explanation of what the variable does." Then we read about an option called ForceSync: "If this option is set to no, ZooKeeper will not require updates to be synced to the media." There is no discussion of risks at all.
Some people know about this but think of it in terms of a broader approach to "using Zookeeper asynchronously". Used asynchronously, Zookeeper lets you start a series of operations but either ignore their termination, or at least not wait one by one. Of course flow control always kicks in eventually, to prevent congestion, but you end up with a stream of requests. In this mode it is nearly universal that you would also set ForceSync=no.
So how safe are such actions?
Elsewhere, on the ZooKeeper blog, Flavio Junquera writes that the system would perfectly well if this option is used, and that it can offer big speedups. He comments that for safety, there are several options: "You could consider using write barriers, or battery-backed raid SSD". The write barrier remark relates to a Linux system call, "fsync". A battery-backed raid SSD is a type of SSD storage with a DRAM cache that can hold pending writes in memory (in DRAM), but with battery backup so that if power fails, the pending writes will definitely complete. Then behind the DRAM are a set of SSD storage units arranged to handle transfers in parallel, so that the aggregate bandwidth might be enough to keep up with the DRAM transfer rates.
On StackOverflow and elsewhere, you can easily find threads encouraging you to configure ZooKeeper with ForceWrites=no, and assuring the reader that nobody has ever observed any bad consequences.
In effect, there is very little discussion of risks, except in the sense of "yes, you should definitely use this feature, but remember to also do these other things...."
So what's the issue, and why is it interesting?
At the core of any Paxos implementation is the transaction log where Paxos stores its state. In Derecho, this takes the form of replicated data residing in the replicated C++ objects defined by the developer. In classic Paxos, it was a list of log entries associated with the "acceptor role". Most people understand this to have been an append-only disk file, but my colleague and friend Robbert van Renesse, a Paxos expert, questions that assumption. He thinks that Leslie was deliberately vague about where the logs live, with the intent that it could equally well be used as an in-memory atomic multicast. Derecho does exactly that: it has one protocol, with two configuration options, and you get to pick. Durable storage on disk gives you a durable Paxos, and in-memory storage, a form of atomic multicast with total ordering and fault-tolerance.
The same is true in ZooKeeper, in which performance centers on the speed of the ZooKeeper transaction log. You need to tell it where you want the log to reside. Some popular options include placing it in RamDisk (in memory), or on a real disk, or perhaps an SSD. Above you saw recommendations that it be on a battery-backed raid SSD.
The problem is that if you just put the log on a normal disk or even a normal SSD disk, you get Paxos guarantees of durability... but you also see a heck of a big slowdown. Partly this is because DMA to an SSD is quite slow compared to copying in memory. But the bigger issue is that each time you do an SSD write, if you actually wait for the write to fully complete ("a forced sync"), you pay a full millisecond just waiting.
Even with concurrency this limits the typical SSD configuration of ZooKeeper to about 1000 write operations per second.
Early in the ZooKeeper story, the developers ran into this issue, and added a new option: ForceSync=no. With it, ZooKeeper "on its own" ceases to be a true Paxos log, because it will build a backlog of in-memory updates queued up to be written to disk, and won't actually carry out those updates instantly. But it gains hugely in performance: 50,000 writes per second become completely feasible. A 50x speedup... at what cost?
This is where those comments about battery-backed SSDs and write barriers enter the picture. And this is the puzzle: in fact, you can use ZooKeeper safely in this mode, at no cost and no risk at all. But it depends on your perception of cost, and of risk.
Lets start by setting ForceWrites=no but ignoring the helpful advice. ZooKeeper will be buggy. But, to be bit by this particular bug two things have to happen. First, you need to have a service that crashes and develops amnesia about a batch of committed transactions (updates) that were pending at the time of the crash. And second, someone or something needs to notice.
The point about "someone noticing" is the key to why so many applications get away with setting ForceSync=no, and yet pay no attention to Flavio's advice. Think about the sequence of events for an application using ZooKeeper. Some application is about not to complete something important, like launching the rocket ship. So it writes to the ZookKeeper log "... two, one, ignition!" and presses the launch button.
Exactly as this occurs, the power goes out, and on recovery, the system has no record that the button was about to get pushed. So we have an inconsistency that Paxos normally doesn't permit: Lamport requires that Paxos must never forget a committed transaction, meaning that once the application is told the commit has occurred, Paxos has an obligation to not lose it.
But this is not a likely failure sequence! The amnesia part, sure, that really is likely. A bit like with a normal Linux file system: if a program crashes before calling fsync, the last bytes it wrote could easily be lost (maybe even the last few thousand). We know that, and learn to call fsync. But someone actually caring, about that specific operation, yet neglecting to manually call fsync? Seems very unlikely...
So here we have ZooKeeper acting... like Linux file systems normally act! In fact, you can manually call fsync anytime you like in ZooKeeper, so if you do need it, there it is. That's the write-barrier approach.
The battery-backed raid SSD option is less common.
So who is wrong: Leslie, for including this rule in the specification? The good user, who learns to call fsync when necessary? Or the bad user, for recklessly breaking the properties of Paxos, all for a lousy 50x or 100x speedup?
As a builder, I have to feel sympathy for any developer who wants the speed. And I honestly question that Paxos specification. Maybe the requirement really is too strong! Couldn't it be reexpressed in terms of fsync: "no committed request will ever be lost if fsync was invoked, and completed after the commit?"
In fact the interesting issue here is that when ForceSync=no, ZooKeeper simply imposes an extra obligation on the behavior of the developer (use fsync, or confirm that you have the right kind of specialized SSD). As we discussed in that prior blog entry, Paxos already imposes obligations on its users, and doesn't express those either. Why is this different?
Yet I also understand Leslie. I've asked him about this, and he thinks developers will just get it wrong. They want the speed, because otherwise they look bad, so they flip this switch, but do something for extra speed in a situation where it really isn't appropriate.
Here in a college town, with students who definitely drive unsafely and fast, I get it.
How many of the developers who push ZooKeeper's insane speed button actually know what they are doing, and think about when to manually call fsync? Yet on the other hand, how many of their applications would break if the ZooKeeper storage subsystem were to slow down by 50x or 100x?
So you tell me: should systems follow the ZooKeeper lead?
Seriously: what do you think? Should Derecho support ForceSync=no?
In a recent blog posting, we discussed some of the missing aspects of that very specification. As a result, when I read the ZooKeeper documentation, I was intrigued to realize that the documentation more or less urges that the system be configured to violate Paxos! In fact the document is short, and easy to read, so have a look if you are skeptical.
You'll learn about all sorts of parameters that represent ZooKeeper's response to those missing specification elements, such as how to deal with disks that fill up completely, or avoiding inconsistency in the list of servers running the ZooKeeper service.
And then, in the middle of the same document, you run into a fascinating option: there is a small section called "Unsafe configuration options" that explains that "The following options can be useful, but be careful when you use them. The risk of each is explained along with the explanation of what the variable does." Then we read about an option called ForceSync: "If this option is set to no, ZooKeeper will not require updates to be synced to the media." There is no discussion of risks at all.
Some people know about this but think of it in terms of a broader approach to "using Zookeeper asynchronously". Used asynchronously, Zookeeper lets you start a series of operations but either ignore their termination, or at least not wait one by one. Of course flow control always kicks in eventually, to prevent congestion, but you end up with a stream of requests. In this mode it is nearly universal that you would also set ForceSync=no.
So how safe are such actions?
Elsewhere, on the ZooKeeper blog, Flavio Junquera writes that the system would perfectly well if this option is used, and that it can offer big speedups. He comments that for safety, there are several options: "You could consider using write barriers, or battery-backed raid SSD". The write barrier remark relates to a Linux system call, "fsync". A battery-backed raid SSD is a type of SSD storage with a DRAM cache that can hold pending writes in memory (in DRAM), but with battery backup so that if power fails, the pending writes will definitely complete. Then behind the DRAM are a set of SSD storage units arranged to handle transfers in parallel, so that the aggregate bandwidth might be enough to keep up with the DRAM transfer rates.
On StackOverflow and elsewhere, you can easily find threads encouraging you to configure ZooKeeper with ForceWrites=no, and assuring the reader that nobody has ever observed any bad consequences.
In effect, there is very little discussion of risks, except in the sense of "yes, you should definitely use this feature, but remember to also do these other things...."
So what's the issue, and why is it interesting?
At the core of any Paxos implementation is the transaction log where Paxos stores its state. In Derecho, this takes the form of replicated data residing in the replicated C++ objects defined by the developer. In classic Paxos, it was a list of log entries associated with the "acceptor role". Most people understand this to have been an append-only disk file, but my colleague and friend Robbert van Renesse, a Paxos expert, questions that assumption. He thinks that Leslie was deliberately vague about where the logs live, with the intent that it could equally well be used as an in-memory atomic multicast. Derecho does exactly that: it has one protocol, with two configuration options, and you get to pick. Durable storage on disk gives you a durable Paxos, and in-memory storage, a form of atomic multicast with total ordering and fault-tolerance.
The same is true in ZooKeeper, in which performance centers on the speed of the ZooKeeper transaction log. You need to tell it where you want the log to reside. Some popular options include placing it in RamDisk (in memory), or on a real disk, or perhaps an SSD. Above you saw recommendations that it be on a battery-backed raid SSD.
The problem is that if you just put the log on a normal disk or even a normal SSD disk, you get Paxos guarantees of durability... but you also see a heck of a big slowdown. Partly this is because DMA to an SSD is quite slow compared to copying in memory. But the bigger issue is that each time you do an SSD write, if you actually wait for the write to fully complete ("a forced sync"), you pay a full millisecond just waiting.
Even with concurrency this limits the typical SSD configuration of ZooKeeper to about 1000 write operations per second.
Early in the ZooKeeper story, the developers ran into this issue, and added a new option: ForceSync=no. With it, ZooKeeper "on its own" ceases to be a true Paxos log, because it will build a backlog of in-memory updates queued up to be written to disk, and won't actually carry out those updates instantly. But it gains hugely in performance: 50,000 writes per second become completely feasible. A 50x speedup... at what cost?
This is where those comments about battery-backed SSDs and write barriers enter the picture. And this is the puzzle: in fact, you can use ZooKeeper safely in this mode, at no cost and no risk at all. But it depends on your perception of cost, and of risk.
Lets start by setting ForceWrites=no but ignoring the helpful advice. ZooKeeper will be buggy. But, to be bit by this particular bug two things have to happen. First, you need to have a service that crashes and develops amnesia about a batch of committed transactions (updates) that were pending at the time of the crash. And second, someone or something needs to notice.
The point about "someone noticing" is the key to why so many applications get away with setting ForceSync=no, and yet pay no attention to Flavio's advice. Think about the sequence of events for an application using ZooKeeper. Some application is about not to complete something important, like launching the rocket ship. So it writes to the ZookKeeper log "... two, one, ignition!" and presses the launch button.
Exactly as this occurs, the power goes out, and on recovery, the system has no record that the button was about to get pushed. So we have an inconsistency that Paxos normally doesn't permit: Lamport requires that Paxos must never forget a committed transaction, meaning that once the application is told the commit has occurred, Paxos has an obligation to not lose it.
But this is not a likely failure sequence! The amnesia part, sure, that really is likely. A bit like with a normal Linux file system: if a program crashes before calling fsync, the last bytes it wrote could easily be lost (maybe even the last few thousand). We know that, and learn to call fsync. But someone actually caring, about that specific operation, yet neglecting to manually call fsync? Seems very unlikely...
So here we have ZooKeeper acting... like Linux file systems normally act! In fact, you can manually call fsync anytime you like in ZooKeeper, so if you do need it, there it is. That's the write-barrier approach.
The battery-backed raid SSD option is less common.
So who is wrong: Leslie, for including this rule in the specification? The good user, who learns to call fsync when necessary? Or the bad user, for recklessly breaking the properties of Paxos, all for a lousy 50x or 100x speedup?
As a builder, I have to feel sympathy for any developer who wants the speed. And I honestly question that Paxos specification. Maybe the requirement really is too strong! Couldn't it be reexpressed in terms of fsync: "no committed request will ever be lost if fsync was invoked, and completed after the commit?"
In fact the interesting issue here is that when ForceSync=no, ZooKeeper simply imposes an extra obligation on the behavior of the developer (use fsync, or confirm that you have the right kind of specialized SSD). As we discussed in that prior blog entry, Paxos already imposes obligations on its users, and doesn't express those either. Why is this different?
Yet I also understand Leslie. I've asked him about this, and he thinks developers will just get it wrong. They want the speed, because otherwise they look bad, so they flip this switch, but do something for extra speed in a situation where it really isn't appropriate.
Here in a college town, with students who definitely drive unsafely and fast, I get it.
How many of the developers who push ZooKeeper's insane speed button actually know what they are doing, and think about when to manually call fsync? Yet on the other hand, how many of their applications would break if the ZooKeeper storage subsystem were to slow down by 50x or 100x?
So you tell me: should systems follow the ZooKeeper lead?
Seriously: what do you think? Should Derecho support ForceSync=no?
Tuesday, 29 August 2017
The adequacy of specifications
I had coffee with a visitor yesterday: Professor Eva Kuhn from the Technical University in Vienna. Our conversation was focused on the power, and limitations, of new methods for creating correct solutions to distributed computing problems.
As you probably know, for many years I've been in dialog with a number of programming language researchers (notably Bob Constable, Mooly Sagiv and Noam Rimsky, although the full list would be much longer and would include Leslie Lamport, Nancy Lynch, Jay Lorch and many others), all specialists on a new way of generating provably correct distributed computing systems and protocols from formal specifications. I'm not an expert on this topic myself -- my close collaborator Robbert van Renesse is far more knowledgeable than me, and actually works with such tools himself. Call me an enthusiast.
The methodology they've worked with is roughly as follows. Using temporal logic or a similar abstract mathematical representation, one creates a description of the problem in terms of sets (the members might be understood as computing nodes, processes, variables, the network itself -- the designer gets to decide), operations upon them, and statements about them. In this way we can model a distributed collection of computers, exchanges of messages between processes running upon them, and even crashes.
Next, one specifies a desired behavior, such as uniform agreement (the abstract problem underlying consensus protocols such as Paxos, including the versions we built into Derecho). In some sense this step describes a "goal", but not the method for achieving the goal. Think of the specification as a set of constraints, assumptions, invariants: properties that characterize a correct solution. Ideally, the behavior would have a safety component ("the solution only does good things, in the following sense...") and a liveness component ("provided that the following assumptions hold, the solution always terminates"). But some protocols aren't always live, and sometimes the conditions under which they are live are difficult to pin down, so this second aspect isn't necessarily feasible.
At any rate, in the penultimate step, one specifies the desired protocol itself, but still in a logic formalism. This is done by expressing the behavior of the protocol as a sequence of operations in the underlying framework -- for example, as a set of temporal logic "actions" on the underlying sets, carefully limited so that any "distributed" operation is performed using our abstracted versions of primitives that make sense in real networks. For example, the standard Paxos protocol, with its leader-based rounds used to construct ballots and contend for slots in the Paxos log, would be transformed into a series of set operations that match the behavior of the leader, the local copies of the logs at each of the acceptor processes, and so forth. The lowest level operations would be formal versions of message send and receive primitives.
With this in hand, the next step is to use a theorem prover like NuPRL (Constable's system) or Ivy (the one used at Tel Aviv University) to prove that the abstractly-specified protocol implements the abstractly-formalized behavioral specification. For example, in the case of Paxos, such a proof would show that for any feasible mix of roles (leader, acceptor, etc), and for every reachable protocol state, the correctness invariants hold. We would also want to show that from any initial state, some decision states are always reachable, but of course this is not always possible. For one thing, the FLP impossibility prevents us from creating a protocol in which a decision is guaranteed to occur within finite time, but in fact there are similar cases in which progress can't occur, namely situations that might involve a crash of a majority of the machines, or a partitioning of the network. For example, if you were to launch a consensus algorithm in a setting where more than half the nodes have crashed, clearly it wouldn't be able to reach consensus. As mentioned above, in the ideal case you actually specify assumptions under which progress can occur ("we assume that at least a majority of the processes are operational and remain operational throughout the execution of the protocol"), but it isn't always as easy as you might expect to specify those assumptions. So sometimes, this aspect is not addressed.
These NuPRL or Ivy (or TLA+, Dafny, Coq, Larch...) proofs are semi-manual. There is a proof-checking step, typically done using a technique called model checking (basically, the system enumerates reachable states and verifies that the invariants hold for all such states). Then there are higher level theorems that can offer short-cuts: general proof cases that were previously proved and checked that essentially represent forms of meta-reasoning, covering a class of behaviors. These allow the checker to avoid repeatedly model-checking basic steps and to instead model-check the pattern, and then look for instances of that pattern. Finally, when the checker stalls, a human can intervene and help it find the proof (or perhaps modify the protocol or the target environment specification, to make it easier to establish the desired property).
The meta-proofs (the higher level ones) are very interesting and necessary, because they potentially address cases that cannot be model-checked by exhaustively enumerating every reachable state. For example, suppose that some protocol can generate unbounded runs of states, but a proof exists that every reachable state satisfies a given property. With that "meta" proof in hand, we don't need to examine every reachable state in order to know that the property always holds, and this might let us make a true statement about the protocol that references the meta-property. In contrast, had we tried to examine every reachable state, the checker would have failed, since the runs are unbounded, hence the number of states needing to be checked is unbounded.
In practice, the power of a tool like Ivy or NuPRL centers on this kind of meta-reasoning, and the sophistication of the tactics used to match proof requirements to the library of meta-proofs. Someday, these tactics may approach the sophistication of a human logician, and in fact NuPRL has already been used to semi-automatically solve some deep open problems in logic! But there are many cases it would not yet be able to tackle.
When checkers fail, they sometimes can exhibit a counterexample: perhaps, a run in which two processes enter "decision" states but hold different outcome values, violating consensus. But they can also simply fail to find a proof. This is because a powerful enough specification language can encode undecidable questions, hence one simply cannot automate the entire proof task: there are guaranteed to be some problems on which a prover can neither conclude that a statement is true, nor false. Moreover, for any finite amount of resources (space, computer time) there are problems that would take much more space, or much more time, to model check. So for several reasons, the checker might stall. If it succeeds, though, the result is that we have a proof for our abstract protocol specification: we can show that it solves the problem, as specified.
An interesting point, tangential to what I really want to say here, is that one could perhaps extract minimum conditions for progress (a form of weakest precondition), in the manner common in PL correctness proofs of a few decades ago. This would automate extraction of assumptions needed to prove "conditional liveness": if the precondition holds, then progress will occur. To me that would be amazing, and would automate a step that Chandra and Toueg first proposed for consensus nearly 20 years ago (the famous <>W oracle). If you love theory and languages, do consider tackling this challenge!
But staying "on message", the last step with a prover such as Ivy or NuPRL is to extract a provably correct program in C or O'CaML from the proof itself. That is, given a specification of the problem, and a specification of the protocol, and a proof that the given protocol solves the problem, these tools let you push a button and automatically extract the corresponding code in an executable form, after which you simply compile and run it! Ideally, the compiler used should be proved correct (there is a proved compiler for a subset of C), and the operating system itself be proved correct (like SEL4), and the hardware verified too (using tools like Verilog) and the foundry that made the chips... well, one goes as far as one can. In fact any chain of technologies has its limitations. But let's not fuss over the obvious.
Professor Kuhn works with people developing safety critical systems for self-driving cars, control of potentially dangerous equipment, and so forth, and for her, this new methodology was fascinating. In fact she isn't the first person I've talked to about this: Chris Hobbs, at QNX, and his colleague Peter Shook, are also extremely interested in the potential of such tools. By taking the programmer out of the loop and extracting code directly from a proof. we seemingly eliminate a weakness in many kinds of control systems, where one historically would hire a team to design a solution, but then would depend on people to write the required code, after which you use a method such as the "B method" to try an prove the code correct. The resulting human-generated proofs are only as good as the human team carrying them out, and the worry always exists that they might have failed to check some important case. With a computer-generated proof, there are computable "checking" methods that can quickly establish whether or not every case was model-checked.
And yet even with automated extraction, issues remain. Can every solvable problem be tackled in this way? Over coffee, Professor Kuhn and I talked about two concerns.
First, there are solvable problems for which a model-checker might run low on space or time and throw up its hands, and hence that could be solved in principle, but in fact might not be amenable to formal treatment even so. So one can imagine situations in which there is some important task, like controlling the flaps on an airplane wing, a good solution that our engineering colleagues want to implement, and a hand-built proof of correctness that "seems" adequate, but for which there isn't any feasible fully-machine checked counterpart, because our computers might not be powerful enough, or perhaps because our techniques for generating model-checked proofs might not have the needed meta-proof methods at hand.
A related issue was raised by Hobbs and Shook at QNX: If a proof (and for that matter, the corresponding C program) is not "natural" in appearance, a human skeptic might not be easily convinced that it is correct. Thus there are also model-checked proofs that might be rejected by a team tasked with confirming that the airplane is safe to fly: the computer says "yes, here is the proof" but the skeptic in the team might worry that if no human can read and fully understand that proof, it could be flawed in some systematic way and yet this would be overlooked.
That concern leads directly to the second question Professor Kuhn and I found intriguing. Our conversation ended on a related form of impasse: suppose that the original problem specification itself is somehow inadequate? For example, one could imagine a specification for behavior of flaps on an airplane wing that leaves out some important case that can actually arise, and hence fails to pin down the correct behavior in that case. Such a specification leaves undefined the correct behavior for some actual situations that might arise in the real world, although perhaps it covers "most" cases and hence might seem complete and useful: you could still generate code, look at examples, trace the logic, and see that for those examples the code behaves properly. The lurking danger would be that because there were unspecified but real cases, examples could also exist in which the behavior would be different than intended, because the specification neglected to cover them.
Thus we would want to be sure that the specification itself was adequate in the sense of fully specifying every case that could really arise in practice. This, though, seems to be a somewhat less fully solved problem. Indeed, it seems to pose an impossible requirement!
I've been shown some work that looks at specifications, and the question is a classic one: large communities are hard at work on the topic, and have been for decades. The issue is that the "adequacy of a specification" problem itself seems to be undecideable. The intuition is sort of obvious: if one could decide all possible adequacy situations, what would stop me from encoding some simple undecideable problem (such as the halting problem), and then using the test of adequacy to solve the undecideable problem? Seemingly, nothing stops me from doing this. Thus adequacy-testing should itself be undecideable. I bet someone has proved this, although I don't think I've ever seen such a paper. I need to read more of the PL literature.
At any rate, what we see here is that on the one hand, our field seems to be at the edge of a major advance (automated synthesis of provably correct solutions to safety-critical systems problems), but on the other hand, is also approaching a natural and final form of impossibility: the risk that for important cases, it may turn out to be impossible to verify that the specification itself is "complete".
There is reason for hope. There are many situations in which if one is given a program and must answer a question about it, the task cannot be solved because the given program might encode an undecideable task. Yet when we use computational methods to generate programs, we can often prove that our methods only generate sound programs.
Could we solve the adequacy problem in this manner? For example, is there a way to generate specifications through some kind of dialog with the developer, that would only generate adequate specifications with full coverage of the problem domain? This, I think, should be possible. The resulting solution might not be able to specify every problem you can dream up, but for the things it could specify, we would know that the specification doesn't overlook any possible scenarios.
Perhaps the practical class of critical control systems doesn't actually require the ability to specify control tasks that encode undecideable questions. If so, then perhaps every needed critical control solution can be created. This would finesse the issue: even though there may be ways to encode undecideability into the same formalism, our more limited use of the methodology would never attempt to do the impossible.
My hope is that we are rapidly heading towards this kind of happy outcome... with all the progress on proofs using NuPRL an Ivy (and other systems like TLA+, Dafny, Larch and Coq), we'll know pretty soon.
As you probably know, for many years I've been in dialog with a number of programming language researchers (notably Bob Constable, Mooly Sagiv and Noam Rimsky, although the full list would be much longer and would include Leslie Lamport, Nancy Lynch, Jay Lorch and many others), all specialists on a new way of generating provably correct distributed computing systems and protocols from formal specifications. I'm not an expert on this topic myself -- my close collaborator Robbert van Renesse is far more knowledgeable than me, and actually works with such tools himself. Call me an enthusiast.
The methodology they've worked with is roughly as follows. Using temporal logic or a similar abstract mathematical representation, one creates a description of the problem in terms of sets (the members might be understood as computing nodes, processes, variables, the network itself -- the designer gets to decide), operations upon them, and statements about them. In this way we can model a distributed collection of computers, exchanges of messages between processes running upon them, and even crashes.
Next, one specifies a desired behavior, such as uniform agreement (the abstract problem underlying consensus protocols such as Paxos, including the versions we built into Derecho). In some sense this step describes a "goal", but not the method for achieving the goal. Think of the specification as a set of constraints, assumptions, invariants: properties that characterize a correct solution. Ideally, the behavior would have a safety component ("the solution only does good things, in the following sense...") and a liveness component ("provided that the following assumptions hold, the solution always terminates"). But some protocols aren't always live, and sometimes the conditions under which they are live are difficult to pin down, so this second aspect isn't necessarily feasible.
At any rate, in the penultimate step, one specifies the desired protocol itself, but still in a logic formalism. This is done by expressing the behavior of the protocol as a sequence of operations in the underlying framework -- for example, as a set of temporal logic "actions" on the underlying sets, carefully limited so that any "distributed" operation is performed using our abstracted versions of primitives that make sense in real networks. For example, the standard Paxos protocol, with its leader-based rounds used to construct ballots and contend for slots in the Paxos log, would be transformed into a series of set operations that match the behavior of the leader, the local copies of the logs at each of the acceptor processes, and so forth. The lowest level operations would be formal versions of message send and receive primitives.
With this in hand, the next step is to use a theorem prover like NuPRL (Constable's system) or Ivy (the one used at Tel Aviv University) to prove that the abstractly-specified protocol implements the abstractly-formalized behavioral specification. For example, in the case of Paxos, such a proof would show that for any feasible mix of roles (leader, acceptor, etc), and for every reachable protocol state, the correctness invariants hold. We would also want to show that from any initial state, some decision states are always reachable, but of course this is not always possible. For one thing, the FLP impossibility prevents us from creating a protocol in which a decision is guaranteed to occur within finite time, but in fact there are similar cases in which progress can't occur, namely situations that might involve a crash of a majority of the machines, or a partitioning of the network. For example, if you were to launch a consensus algorithm in a setting where more than half the nodes have crashed, clearly it wouldn't be able to reach consensus. As mentioned above, in the ideal case you actually specify assumptions under which progress can occur ("we assume that at least a majority of the processes are operational and remain operational throughout the execution of the protocol"), but it isn't always as easy as you might expect to specify those assumptions. So sometimes, this aspect is not addressed.
These NuPRL or Ivy (or TLA+, Dafny, Coq, Larch...) proofs are semi-manual. There is a proof-checking step, typically done using a technique called model checking (basically, the system enumerates reachable states and verifies that the invariants hold for all such states). Then there are higher level theorems that can offer short-cuts: general proof cases that were previously proved and checked that essentially represent forms of meta-reasoning, covering a class of behaviors. These allow the checker to avoid repeatedly model-checking basic steps and to instead model-check the pattern, and then look for instances of that pattern. Finally, when the checker stalls, a human can intervene and help it find the proof (or perhaps modify the protocol or the target environment specification, to make it easier to establish the desired property).
The meta-proofs (the higher level ones) are very interesting and necessary, because they potentially address cases that cannot be model-checked by exhaustively enumerating every reachable state. For example, suppose that some protocol can generate unbounded runs of states, but a proof exists that every reachable state satisfies a given property. With that "meta" proof in hand, we don't need to examine every reachable state in order to know that the property always holds, and this might let us make a true statement about the protocol that references the meta-property. In contrast, had we tried to examine every reachable state, the checker would have failed, since the runs are unbounded, hence the number of states needing to be checked is unbounded.
In practice, the power of a tool like Ivy or NuPRL centers on this kind of meta-reasoning, and the sophistication of the tactics used to match proof requirements to the library of meta-proofs. Someday, these tactics may approach the sophistication of a human logician, and in fact NuPRL has already been used to semi-automatically solve some deep open problems in logic! But there are many cases it would not yet be able to tackle.
When checkers fail, they sometimes can exhibit a counterexample: perhaps, a run in which two processes enter "decision" states but hold different outcome values, violating consensus. But they can also simply fail to find a proof. This is because a powerful enough specification language can encode undecidable questions, hence one simply cannot automate the entire proof task: there are guaranteed to be some problems on which a prover can neither conclude that a statement is true, nor false. Moreover, for any finite amount of resources (space, computer time) there are problems that would take much more space, or much more time, to model check. So for several reasons, the checker might stall. If it succeeds, though, the result is that we have a proof for our abstract protocol specification: we can show that it solves the problem, as specified.
An interesting point, tangential to what I really want to say here, is that one could perhaps extract minimum conditions for progress (a form of weakest precondition), in the manner common in PL correctness proofs of a few decades ago. This would automate extraction of assumptions needed to prove "conditional liveness": if the precondition holds, then progress will occur. To me that would be amazing, and would automate a step that Chandra and Toueg first proposed for consensus nearly 20 years ago (the famous <>W oracle). If you love theory and languages, do consider tackling this challenge!
But staying "on message", the last step with a prover such as Ivy or NuPRL is to extract a provably correct program in C or O'CaML from the proof itself. That is, given a specification of the problem, and a specification of the protocol, and a proof that the given protocol solves the problem, these tools let you push a button and automatically extract the corresponding code in an executable form, after which you simply compile and run it! Ideally, the compiler used should be proved correct (there is a proved compiler for a subset of C), and the operating system itself be proved correct (like SEL4), and the hardware verified too (using tools like Verilog) and the foundry that made the chips... well, one goes as far as one can. In fact any chain of technologies has its limitations. But let's not fuss over the obvious.
Professor Kuhn works with people developing safety critical systems for self-driving cars, control of potentially dangerous equipment, and so forth, and for her, this new methodology was fascinating. In fact she isn't the first person I've talked to about this: Chris Hobbs, at QNX, and his colleague Peter Shook, are also extremely interested in the potential of such tools. By taking the programmer out of the loop and extracting code directly from a proof. we seemingly eliminate a weakness in many kinds of control systems, where one historically would hire a team to design a solution, but then would depend on people to write the required code, after which you use a method such as the "B method" to try an prove the code correct. The resulting human-generated proofs are only as good as the human team carrying them out, and the worry always exists that they might have failed to check some important case. With a computer-generated proof, there are computable "checking" methods that can quickly establish whether or not every case was model-checked.
And yet even with automated extraction, issues remain. Can every solvable problem be tackled in this way? Over coffee, Professor Kuhn and I talked about two concerns.
First, there are solvable problems for which a model-checker might run low on space or time and throw up its hands, and hence that could be solved in principle, but in fact might not be amenable to formal treatment even so. So one can imagine situations in which there is some important task, like controlling the flaps on an airplane wing, a good solution that our engineering colleagues want to implement, and a hand-built proof of correctness that "seems" adequate, but for which there isn't any feasible fully-machine checked counterpart, because our computers might not be powerful enough, or perhaps because our techniques for generating model-checked proofs might not have the needed meta-proof methods at hand.
A related issue was raised by Hobbs and Shook at QNX: If a proof (and for that matter, the corresponding C program) is not "natural" in appearance, a human skeptic might not be easily convinced that it is correct. Thus there are also model-checked proofs that might be rejected by a team tasked with confirming that the airplane is safe to fly: the computer says "yes, here is the proof" but the skeptic in the team might worry that if no human can read and fully understand that proof, it could be flawed in some systematic way and yet this would be overlooked.
That concern leads directly to the second question Professor Kuhn and I found intriguing. Our conversation ended on a related form of impasse: suppose that the original problem specification itself is somehow inadequate? For example, one could imagine a specification for behavior of flaps on an airplane wing that leaves out some important case that can actually arise, and hence fails to pin down the correct behavior in that case. Such a specification leaves undefined the correct behavior for some actual situations that might arise in the real world, although perhaps it covers "most" cases and hence might seem complete and useful: you could still generate code, look at examples, trace the logic, and see that for those examples the code behaves properly. The lurking danger would be that because there were unspecified but real cases, examples could also exist in which the behavior would be different than intended, because the specification neglected to cover them.
Thus we would want to be sure that the specification itself was adequate in the sense of fully specifying every case that could really arise in practice. This, though, seems to be a somewhat less fully solved problem. Indeed, it seems to pose an impossible requirement!
I've been shown some work that looks at specifications, and the question is a classic one: large communities are hard at work on the topic, and have been for decades. The issue is that the "adequacy of a specification" problem itself seems to be undecideable. The intuition is sort of obvious: if one could decide all possible adequacy situations, what would stop me from encoding some simple undecideable problem (such as the halting problem), and then using the test of adequacy to solve the undecideable problem? Seemingly, nothing stops me from doing this. Thus adequacy-testing should itself be undecideable. I bet someone has proved this, although I don't think I've ever seen such a paper. I need to read more of the PL literature.
At any rate, what we see here is that on the one hand, our field seems to be at the edge of a major advance (automated synthesis of provably correct solutions to safety-critical systems problems), but on the other hand, is also approaching a natural and final form of impossibility: the risk that for important cases, it may turn out to be impossible to verify that the specification itself is "complete".
There is reason for hope. There are many situations in which if one is given a program and must answer a question about it, the task cannot be solved because the given program might encode an undecideable task. Yet when we use computational methods to generate programs, we can often prove that our methods only generate sound programs.
Could we solve the adequacy problem in this manner? For example, is there a way to generate specifications through some kind of dialog with the developer, that would only generate adequate specifications with full coverage of the problem domain? This, I think, should be possible. The resulting solution might not be able to specify every problem you can dream up, but for the things it could specify, we would know that the specification doesn't overlook any possible scenarios.
Perhaps the practical class of critical control systems doesn't actually require the ability to specify control tasks that encode undecideable questions. If so, then perhaps every needed critical control solution can be created. This would finesse the issue: even though there may be ways to encode undecideability into the same formalism, our more limited use of the methodology would never attempt to do the impossible.
My hope is that we are rapidly heading towards this kind of happy outcome... with all the progress on proofs using NuPRL an Ivy (and other systems like TLA+, Dafny, Larch and Coq), we'll know pretty soon.
Subscribe to:
Posts (Atom)