[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)