[HN Gopher] Paxos automatically determined safe and secure ___________________________________________________________________ Paxos automatically determined safe and secure Author : rbanffy Score : 51 points Date : 2021-10-27 20:55 UTC (2 hours ago) (HTM) web link (news.umich.edu) (TXT) w3m dump (news.umich.edu) | jt_thurs_82 wrote: | > the most foundational distributed computing protocols--known as | Paxos--meets its specifications. | | > Paxos is one of the most important examples of the category | | >"Most--if not all--consensus algorithms fundamentally derive | concepts from Paxos," Goel said. | | A lot of burying the lede here, trying to imply Paxos powers many | more applications than it actually does. While Paxos is in decent | widespread use, and influential, I find some of the verbiage here | lying by omission. | Jweb_Guru wrote: | That seems pretty accurate, TBH. Correct distributed consensus | is almost exclusively done via some flavor of Paxos. | | As for the actual research, it probably needs much closer | reading, but if they can automatically infer nontrivial | inductive invariants that's _huge_ for automatic verification, | since this is the usual stumbling block for those kinds of | tools. | [deleted] | threatofrain wrote: | Towards an Automatic Proof of Lamport's Paxos (2021) | | https://arxiv.org/pdf/2108.08796.pdf | 0xbadcafebee wrote: | When people talk about security vulnerabilities, they focus on | the most glaring holes. "Memory safety!!!!!" etc. Meanwhile, | cyber criminals merrily go about their day hijacking massive | computer systems without even using a memory safety vuln. Because | the criminals don't give a crap what _kind_ of holes there are - | they any kind will do. | | When people talk about distributed consensus algorithms, they're | similarly missing the important point. A useful algorithm isn't | the end-all be-all of the system. What's important is that the | entire system be operated to a high degree of reliability in a | way that meets the needs of a specific application. Paxos or not, | if your implementation keeps falling over for reasons _other than | consensus_ , or you don't build in the tools to properly deal | with the knock-on effects of consensus issues, etc, then the | whole thing is going to blow up anyway. | | No algorithm on its own will make a better system. You need all | the other parts of the system to be just as awesome, or it falls | apart just the same. | tester756 wrote: | https://xkcd.com/538/ | throw10920 wrote: | Assuming it's possible for most proofs to become automatically | generated (which I don't think is a given), then it seems like | verification work will shift from manually writing proofs into | writing the specification from which proofs will automatically be | generated - in which case, verification engineers will be able to | look forward to an exciting future of figuring out how to tell | the computer what is meant by "is". | | Or doing system implementation directly - it doesn't seem like | automated program synthesis is going anywhere fast... | | (I jest, while still growing to be more of a fan of type systems, | borrow checkers, and formal proofs) ___________________________________________________________________ (page generated 2021-10-27 23:00 UTC)