7 ms·
Three ways formally verified code can go wrong in practice
- jonathanstrange 1y agoNo hardware failure is considered? No cosmic rays flipping bits? No soft or hard real-time guarantees are discussed? What about indeterminate operations that can fail such as requesting memory from some operating system dynamically? I'm asking because I thought high integrity systems are generally evaluated and certified as a combination of hardware and software. Considering software alone seems pretty useless.
- codebje 1y agoSpecifications that are formally verified can definitely cover real-time guarantees, behaviour under error returns from operations like allocation, and similar things. Hardware failures can be accounted for in hardware verification, which is much like software verification: specification + hardware design = verified design; if the spec covers it, the verification guarantees it. Considering software alone isn't pretty useless, nor is having the guarantee that "inc x = x - 1" will always go from an Int to an Int, even if it's not "fully right" at least trying to increment a string or a complex number will be rejected at compile time. Giving up on any improvements in the correctness of code because it doesn't get you all the way to 100% correct is, IMO, defeatist. (Giving up on it because it has diminishing returns and isn't worth the effort is reasonable, of course!)
- charcircuit 1y agoHardware verification doesn't prevent hardware failures. There is a reason RAM comes with ECC. It's not because RAM designers are too lazy to do formal verification. Even with ECC RAM, bit flips can still happen if multiple bits flip at the same time. There are also things like CPUs taking the wrong branch that occasionally happen. You can't assume that the hardware will work perfectly in the real world and have to design for failure.
- jojomodding 1y agoDesigning around hardware failure in software seems cumbersome to insane. If the CPU can randomly execute arbitrary code because it jumps to wherever, no guarantees apply. What you actually do here is consider the probability of a cosmic ray flip, and then accept a certain failure probability. For things like train signals, it's one failure in a billion hours.
- charcircuit 1y agoYet, big sites like Google or TikTok constantly deal with hardware failures everyday while keeping their services and apps running.
- spartanatreyu 1y agoAn approach that has been taken for hardware in space is to have 3 identical systems running at the same time. Execution continues while all systems are in agreement. If a cosmic ray causes a bit-flip in one of the systems, the system not in agreement with the other two takes on the state of the other two and continues. If there is no agreement between all 3 systems, or the execution ends up in an invalid state, all systems restart.
- pixl97 1y ago>Designing around hardware failure in software seems cumbersome to insane I mean there are places to do it. For example ZFS and filesystem checksums. If you've ever been bit by a hard drive that says everything is fine but returns garbage you'll appreciate it.
- kragen 1y ago> Designing around hardware failure in software seems cumbersome to insane. Yet for some reason you chose to post this comment over TCP/IP! And I'm guessing you loaded the browser you typed it in from an SSD that uses ECC. And probably earlier today you retrieved some data from GFS, for example by making a Google search. All three of those are instances of software designed around hardware failure.
- westurner 1y agoSide channels? Is best out of 2 sufficient or is best out of 3 necessary? From https://news.ycombinator.com/context?id=39938759 https://news.ycombinator.com/context?id=39938759 re: s2n-tls: > [ FizzBee, Nagini, Deal-solver, Dafny; icontract, pycontracts, Hoare logic, DbC Design-by-Contract, invariants, parallelism and concurrency and locks, io latency, pass by reference in distributed systems, "FaCT: A DSL for Timing-Sensitive Computation" and side channels [in hw and software] https://news.ycombinator.com/item?id=38527663 https://news.ycombinator.com/item?id=38527663 ] There are so many things to consider; /? awesome-safety https://westurner.github.io/hnlog/#search:awesome-safety https://westurner.github.io/hnlog/#search:awesome-safety : awesome-safety-critical: https://awesome-safety-critical.readthedocs.io/en/latest/ https://awesome-safety-critical.readthedocs.io/en/latest/ Hazard (logic) https://en.wikipedia.org/wiki/Hazard_(logic) https://en.wikipedia.org/wiki/Hazard_(logic) Hazard (computer architecture); out-of-order execution and delays: https://en.wikipedia.org/wiki/Hazard_(computer_architecture) https://en.wikipedia.org/wiki/Hazard_(computer_architecture) Soft error: https://en.wikipedia.org/wiki/Soft_error https://en.wikipedia.org/wiki/Soft_error SEU: Single-Event Upset: https://en.wikipedia.org/wiki/Single-event_upset https://en.wikipedia.org/wiki/Single-event_upset And then cosmic ray and particle physics
- skybrian 1y agoFor portable libraries and apps, there's only so much you can do. However, there are some interesting properties you can prove assuming the environment behaves according to a spec.
- themafia 1y agoEven then you have other physical issues to consider. This is one of the things I love about the Space Shuttle. It had 5 computers for redundancy during launch and return. You obviously don't want to put them all in the same place so you spread them out among the avionics bays. You also obviously don't want them all installed in the same orientation so you install them differently with respect to the vehicles orientation. You also have a huge data network that requires redundancy and you take all the same steps with the multiplexers as well.
- cpgxiii 1y agoThe best example on the Shuttle were the engine control computers. Each engine had two controllers, primary and backup, each with its own set of sensors in the engine itself and each consisting of a lock-step pair of processors. For each engine, the primary controller would use processors built by one supplier, while the backup would use processors of the same architecture but produced by an entirely different supplier (Motorola and TRW). Today, even fairly standard automotive ECUs use dual-processor lock-step systems; a lot the the Cortex-R microcontrollers on the market are designed around enabling dual-core lock-step use, with error/difference checking on all of the busses and memory.
- naasking 1y agoRequiring specialized hardware seems overly strict now that we can handle such things at a higher level via something like the fault tolerant lambda calculus.
- me_again 1y agoBut what do you do when the primary and backup disagree?
- cpeterso 1y agoThis question is posed in Segal’s Law: A man with a watch knows what time it is. A man with two watches is never sure. https://en.wikipedia.org/wiki/Segal%27s_law https://en.wikipedia.org/wiki/Segal%27s_law
- kragen 1y agoThe article does consider hardware failure, yes.
- ip26 1y agoNowhere does the article claim that: "formal verification of the code" -> "high integrity system" Formal verification is simply a method of ensuring your code behaves how you intend. Now, if you want to formally verify your program can tolerate any number of bits flip on any variables at any moment(s) in time, it will happily test this for you. Unfortunately, assuming presently known software methods, this is an unmeetable specification :)
- ip26 1y agoIs asserting the assumptions during code execution not standard practice for formally verified code?
- ngruhn 1y agoHow would that look like if you accidentally assumed you have arbitrary large integers but in practice you have 64 bits?
- appellations 1y agoAdd(x,y): Assert( x >= 0 && y>= 0 ) z = x + y Assert( z >= x && z >= y ) return z There’s definitely smarter ways to do this, but in practice there is always some way to encode the properties you care about in ways that your assertions will be violated. If you can’t observe a violation, it’s not a violation https://en.wikipedia.org/wiki/Identity_of_indiscernibles https://en.wikipedia.org/wiki/Identity_of_indiscernibles
- deleted 1y ago[deleted]
- bluGill 1y agoIn some languages overflow is asserted as a can't happen and so the optimizer will remove your checks
- appellations 1y agoCare to share a language where the compiler infers the semantic meaning of asserts and optimizes them away? I’ve never heard of this optimization.
- MindSpunk 1y agoSigned overflow is UB in C/C++ and several compilers will skip explicit overflow checks as a result. See: https://godbolt.org/z/WehcWj3G5 https://godbolt.org/z/WehcWj3G5
- skybrian 1y agoMany interesting statements aren't a property of the code alone. They're a property of the code when it's run in a particular environment. If you want the proof to be portable then it should only make assumptions that are true in any environment.
- dapperdrake 1y agoNo assumption holds for all environments. Posh example: Axiom of choice.
- naasking 1y agoThere are definitely some assumptions that hold for all environments. For instance, "all resources are finite".
- rook_line_sinkr 1y agoI got told to use these words back in uni verification - Are we building the software right? validation - Are we building the right software? makes many a thing easier to talk about at work
- moandcompany 1y agoYep... Along with this Verification aligns with a specification. E.g. verify if what was implemented matches what was specified. Validation aligns with a requirement. E.g. verify if what was implemented solves the actual problem.
- friendzis 1y agoEngineering specifications implement requirements. EDIT: more formally, specification is a document stating requirements
- ijustlovemath 1y agoUsually there's a separate document that has the requirements, and from that document you have a "software detailed design" which has the specifications for how to build the software such that it upholds the requirements. Subtle but important difference.
- tirant 1y agoI like to talk about goals and not requirements. What is your product goal? Both for the customer (solving a problem) and for the company(solve a marketing need, make money)? Can you proof that you are meeting both? Then you are validating your goals successfully. Most of the time products are missing defined goals, so lots of people have no idea what the fuck they are developing and everyone ends up with their own idea of the product.
- dapperdrake 1y agoThere is an important and distinct pair of definitions used by a possibly smaller but significant number of people: Verification: formal theoretical proof Validation: Empirical test based approach
- stephenlf 1y agoThis is incredible. This post led me to your GitHub, which is full of similarly incredible content. “Awesome Cold Showers”? Beautiful.
- huflungdung 1y ago[dead]
- 0xDEAFBEAD 1y ago>properties like all x in Int: inc(x) > x. Why not just use an assertion? It costs more at runtime, but it's far less dev time than developing a proof, right?
- mrkeen 1y agoNearly everything that goes wrong for me in prod is already a crash/stacktrace, which is what an assertion does. The point of proofs is to not get yourself (or the customer) into that point in the first place.
- kryptiskt 1y agoIt's not a substitute, an assertion only makes sure that it doesn't happen unnoticed, a proof says that it doesn't happen at all. I might prefer to know that my reactor control system has no overflow ahead of time, rather than getting an assertion and crashing if it happens (though it would be a bad reactor control system if it couldn't handle crashes).
- 0xDEAFBEAD 1y agoOK, but that's a reactor control system. If your application has no time-critical aspect, is there any good reason to prefer a proof over an assert?
- dbdr 1y agoWill your users be happier to get an assertion failure when they run your code, compared to no error? (the tradeoff of course being that they might get your code later because it took more time to prove the code is correct)
- 0xDEAFBEAD 1y agoWhat if it's an internal tool, where correctness matters a lot, but failures matter little? E.g. roll back all database changes in case of assertion failure. Perhaps an accounting thing or something of that nature.
- js8 1y agoFormal verification is ultimately an epistemological problem, how do we know that our model of reality corresponds to reality? People have commented that validation is different from verification, but I think validation can be done by formally specifying the environment the program runs in. For example, the question whether user can do X in your software corresponds to a question, is there a sequence of user inputs such that the software plus operating system leads to the output X. By including the environment (like the operating system) into the formal spec we could answer (in theory) such questions. Even if the question is fuzzy, we can today formalize it with AI models. For example, if we ask, does paint program allow user to draw a rose? We can take a definition of a rose from a neural network that recognizes what a rose is, and formally verify the system of paint program and rose verifier given by the NN.
- ThreeFx 1y agoNow you’ve just shifted the problem to a much harder statement: proving the things the NN recognizes as a rose is actually a rose. You cannot get rid of the enviroment, and the best thing you can do is be explicit in what you rely on. For example, formally verified operating systems often rely on hardware correctness, even though the errata sheets for modern CPUs are hundreds of pages long.
- lstodd 1y agoRight, the problem is that one can't formally describe the environment, and any one thing has to interact with it. So formallness goes right out the window.
- js8 1y agoYeah. That's why I am saying it's the epistemological problem. In the above example, that NN recognizes rose as a rose is an assumption that it is correct as a model of the (part of the) world. On that assumption, we get a formal definition of "an image of a rose in the pixelated image", and we use that to formally prove our system allows roses to be painted. But getting rid of that assumption is I believe epistemologically impossible; you have to assume some other correspondence with reality. I agree with you on the hardware. I think the biggest obstacle to software formal correctness is the lack of formal models of which we can be confident describe our environment. (One obstacle is the IP laws - companies do not like to share the models of things they produce.)
- unwind 1y agoThis was very nice, well-written and good-looking (to me) content. Thanks! There was some meta-bug with encoding which almost is like an internal joke but I don't think it's intentional. The Haskell code examples have: inc :: Int -> Int several times, and that `>` entity should very likely just be a `<` in the source code.
- AndrewDucker 1y agoNit: ">"
- ocelotBridge 1y agoFormal verification is great, but cosmic rays don't read our specs.
- addaon 1y agoThey do if they’re in the specs. See near-universal use of lockstep processors, ECC etc in safety-critical and high radiation cases, which comes from the two requirements that “a single bit flip from a cosmic ray shall be detectable” and “multiple simultaneous hit flips from cosmic rays shall be shown to be sufficiently rare in the operating environment.”
- deleted 1y ago[deleted]
- GuB-42 1y agoObligatory quote: "Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth Source: https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf From a quick look at it, it seems to be a "case 1" potential error, as the proof is done by hand. That is the warning is likely because it is a mathematical exercise first, and the code is for illustration and not for inclusion in production software.
- hshdhdhehd 1y agoThis is why one would prefer to run. NGINX over a formally verified http server.
- deleted 1y ago[deleted]
- dinkelberg 1y agoI would recommend reading the post that Hillel is responding to instead, namely Luke Plant's "Breaking 'provably correct' Leftpad" (https://lukeplant.me.uk/blog/posts/breaking-provably-correct-leftpad/ https://lukeplant.me.uk/blog/posts/breaking-provably-correct...).
- Joker_vD 1y ago> I wrote that the "binary search" bug happened because they proved the wrong property, but you can just as well argue that it was a broken assumption (that integers could not overflow). No, you can't argue that (well, argue that successfully). If you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are! The integers do overflow in Java, that's explicitly stated in the Java's spec.
- failrate 1y agoThe article did not also point out issues like the compiler or interpreter having a runtime error, the hardware the software is running on having a defect, etc. Do we consider these out of scope of the discussion?
- xlii 1y agoThere's this place for formal proving that most people won't get to and think it's stupid. I was such person some time ago, but then started to work on the system that: Required 2-3 months for implementation, had no room for error, made processing mistakes cost in thousands of Euros (even silly things). Than you start to wonder "hmmm... how can I use something better than just good practices and judgement? How can I _prove_ design A works". And usually there are tangible problems to avoid: Ensuring that money won't get lost in transaction. Making sure that legal paperwork will be delivered or returned on time. Or that CSV file costing arm and leg for a single row won't have more rows than necessary. Many of these problems are borderline paradoxical. It's known that (as with Two Generals) there are no complete solutions. Usually it's like playing a catch with reality. A game that goes "what happens if we duplicate money mid-flight?" - "which system is source of truth in case of fraud", "do we rather risk false negative or accept MIA state" etc. Sure, it's fun to model a crossroad with streetlights and a chicken just for kicks, but the main "why?" for formal proving is having "this design is good because I've seen the proof of it" moment. But what kind of questions are asked is just as important. I can bet asbestos met all the standards it was checked against :)
- butlike 1y agoYou're touching on a timeless approach which is currently not possible, given the limits of reality. You'd need to know for a fact all potential outlays in order to make sure every change your program (creation) creates is accounted for and proved against. Since you do not have perfect information, your proof, by current definition, cannot be proved to be perfect.
- xlii 1y agoThat's true, just as I cannot possibly measure car speed given innate measuring error which is not a defense from getting a speeding ticket. Formal proving isn't about getting to "my model is reality" but having step above mere imagination or educated guess. That's why it's possible to model paradoxical models. Given N systems they all can fail at the same time and there's nothing that can be done to guarantee message RECV+ACK. So at some point there's invariant saying "ok, we say that 3 out of 5 systems will always work". If you break invariant all hell is loose but at that point many weird stuff might happen. Usually when one needs to think about message passing in a way like [0] formal proving can save lives (or bottoms, depending on the context). [0]: https://xlii.space/eng/network-scenarios/ https://xlii.space/eng/network-scenarios/
- mrkeen 1y ago"The assumptions are wrong" is an unsatisfying "catch-all": compiler, hardware, environment, concurrency bugs. Here's one that's been bugging me lately: Dekker's algorithm (mutual exclusion / critical section) won't work on modern hardware. CPUs are free to rearrange reads and writes such that they still make sense under single-threaded conditions. It's kind of put me off learning about lockfree/lockless programming. Even if I make a machine-checked proof that my concurrent code races only in acceptable ways, I have no way of knowing which instructions will be re-ordered, invalidating the proof.
- layer8 1y agoDekker's algorithm will work on modern hardware if you make use of the appropriate memory barriers. Memory barriers are essential for lock-free algorithms, so I’m not sure why that is putting you off learning them. They are, in a way, an embodiment of the assumptions underlying the algorithms, including Decker’s.