5 ms·

Is there any production software in the world that is written and maintained in a formally verified language? I have only ever seen toy problems and simplified

Is there any production software in the world that is written and maintained in a formally verified language? I have only ever seen toy problems and simplified subsystems of real projects verified. I work on space craft flight software and exactly none of it is formally verified. As far as I know, it's not practical to do so. If we could do it (without ballooning cost and schedule 10x), we would.

arianvanp 7y ago
Amazon S3 and DynamoDB come to mind are good examples. They are model-checked in TLA+ though the applications themselves are not written in TLA+. A large portion of Microsoft's in house developed device drivers for windows are formally verified. Boeing together with DARPA built an autonomous helicopter on top of the formally verified Sel4 microkernel https://ts.data61.csiro.au/projects/TS/SMACCM/ https://ts.data61.csiro.au/projects/TS/SMACCM/ Another one: Wireguard uses formally verified implementations of ed25519 https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star
- 0xffff2 7y ago
  >Amazon S3 and DynamoDB come to mind are good examples. They are model-checked in TLA+ though the applications themselves are not written in TLA+. Honest question (I obviously don't have a ton of experience in this area), what does "model-checked in TLA+ though the applications themselves are not written in TLA+" mean (in terms of the guarantees you're getting)? If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the application code? The HACL* project looks interesting. I would definitely accept that as an affirmative answer to my original question.
  - hwayne 7y ago
    > If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the application code? Code review! So, SO much code review. Also testing and type systems and linters and code review. (There's also some work on automatic synthesis, like PGo, but that's all very, very far from being production-ready.) The main benefit of using TLA+ is that it lets you hammer out issues in the high-level design. Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Turns out that lots of the nastiest bugs are in the design, not the implementation, so using TLA+ saves a lot of time and money. But you still need to code review!
    - 0xffff2 7y ago
      >Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! >Turns out that lots of the nastiest bugs are in the design, not the implementation I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all.
      - hwayne 7y ago
        > Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! I'd _hope_ you'd have those processes, working on space flight and all :P. Good processes > good tools. It's easier to start using a good tool than overhaul your process. So for people who don't have that kind of discipline or heavyweight process, TLA+ gives a lot of benefits for really cheap. AWS, for example, found it really easy to slot into their workflow. Re buffer overruns, I just remembered OpenComRTOS, which used TLA+ to verify low-level properties of their code.[1] They found it super helpful. > I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all. 'Fraid it probably can't help you with the SI units. I'm thinking about "design bugs" more like this: > 1. Suppose we have a document with version 57 > 2. A bulk of delete and reindex will remove the index-v57, increase the version to 58 (for the delete operation), then put a new doc with version 59. While the engine places the index-59 into the version map, the safe-access flag is flipped over (due to a concurrent fresh), the engine won't put that index entry into the version map, but also leave the delete-58 tombstone in the version map. The delete-58 tombstone is stale because the latest version of that document is index-59. > 3. Another bulk of delete and reindex will increase the version to 59 (for a delete) but won't remove docs from Lucene because of the existing (stale) delete-58 tombstone. The index operation will append document (version 60) to Lucene (instead of overwriting). At this point, we will have two documents with the same id. Which was a bug TLA+ found in ElasticSearch.[2] [1]: https://dl.acm.org/doi/10.5555/1779934.1779955 https://dl.acm.org/doi/10.5555/1779934.1779955 [2]: https://github.com/elastic/elasticsearch/issues/31976#issuecomment-404722753 https://github.com/elastic/elasticsearch/issues/31976#issuec...
- candiodari 7y ago
  TLA+: you mean the transitions of one variable are formally proven. Whilst a plus, this is not that different from how compilers were written since the 1980s. Never saw any crash happen there. You should think of these systems like you think of garbage collection. They lower (sometimes eliminate) one particular kind of problem, and that's it. It does not prove the code works, doesn't OOM, doesn't segfault, doesn't dos itself, doesn't enter infinite loop, etc.
zytek 7y ago
AWS S3, as far as I know
- hwayne 7y ago
  The design of S3 was formally specified, but not the actual code.
rurban 7y ago
I would count Simulink RT as formally sound and safe, because you can only wire matching boxes together. Graphically. It's the standard in Automotive, flight stuff also I heard.
- 0xffff2 7y ago
  I do actually have a bit of Simulink generated code in my current project. I absolutely do not consider it to be formally anything. It's one of the highest risk areas of the project IMO because it is very complex and a very black box.
  - magduf 7y ago
    I worked with a Simulink-generated system in a previous job. The generated code was absolutely unreadable by humans, and honestly downright ugly. I agree, it is very high-risk because it is a black box.
- vsskanth 7y ago
  I've used Simulink to model dynamic systems. I would say the C code it generates is "safe" in terms of memory access that can be used for embedded systems, but it does not check for undefined control behavior.
  - rurban 7y ago
    I did not only use it, I generated a C++ compiler backend for it. Of course is generated code ugly, that's not the point. It's generated. Logical problems (and problems in C extensions) are of course always possible, therefore you have Stateflow and other methods. Other formal methods cannot guarantee that neither.
DoingIsLearning 7y ago
The Ada language allows for a subset of the language called SPARK (not to be confused with the Java framework). In Ada you can do Design-by-contract but in the SPARK subset you can actually formally prove the implementation's correctness. SPARK is used to my knowledge in rail signalling system, air traffic control systems, Class III medical devices, and now also NVDIA plans to use it for sections of their ADAS platform. I think the cost aspect is overblown. The biggest issue is that anything related to Ada is not really that well known and often what is known is based on stereotypes from the 80's. Also for most people they would not see it as career growth move to switch to an Ada based technology stack.
hwayne 7y ago
seL4 comes to mind. Also IronFleet[1], which is small but end-to-end verified in Dafny. People tend to verify the cores of complex systems, not the entire thing. See here[2] for more on that. I suspect there'd be a lot of stuff using either SPARK or Event-B, but Tokeneer[3] is the only thing I found with five minutes of Googling. [1]: https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle... [2]: https://www.cs.purdue.edu/homes/pfonseca//papers/eurosys2017-dsbugs.pdf https://www.cs.purdue.edu/homes/pfonseca//papers/eurosys2017... [3]: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer

arianvanp 7y ago

Amazon S3 and DynamoDB come to mind are good examples. They are model-checked in TLA+ though the applications themselves are not written in TLA+. A large portion of Microsoft's in house developed device drivers for windows are formally verified. Boeing together with DARPA built an autonomous helicopter on top of the formally verified Sel4 microkernel https://ts.data61.csiro.au/projects/TS/SMACCM/ https://ts.data61.csiro.au/projects/TS/SMACCM/ Another one: Wireguard uses formally verified implementations of ed25519 https://github.com/project-everest/hacl-star https://github.com/project-everest/hacl-star

0xffff2 7y ago
>Amazon S3 and DynamoDB come to mind are good examples. They are model-checked in TLA+ though the applications themselves are not written in TLA+. Honest question (I obviously don't have a ton of experience in this area), what does "model-checked in TLA+ though the applications themselves are not written in TLA+" mean (in terms of the guarantees you're getting)? If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the application code? The HACL* project looks interesting. I would definitely accept that as an affirmative answer to my original question.
- hwayne 7y ago
  > If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the application code? Code review! So, SO much code review. Also testing and type systems and linters and code review. (There's also some work on automatic synthesis, like PGo, but that's all very, very far from being production-ready.) The main benefit of using TLA+ is that it lets you hammer out issues in the high-level design. Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Turns out that lots of the nastiest bugs are in the design, not the implementation, so using TLA+ saves a lot of time and money. But you still need to code review!
  - 0xffff2 7y ago
    >Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! >Turns out that lots of the nastiest bugs are in the design, not the implementation I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all.
    - hwayne 7y ago
      > Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! I'd _hope_ you'd have those processes, working on space flight and all :P. Good processes > good tools. It's easier to start using a good tool than overhaul your process. So for people who don't have that kind of discipline or heavyweight process, TLA+ gives a lot of benefits for really cheap. AWS, for example, found it really easy to slot into their workflow. Re buffer overruns, I just remembered OpenComRTOS, which used TLA+ to verify low-level properties of their code.[1] They found it super helpful. > I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all. 'Fraid it probably can't help you with the SI units. I'm thinking about "design bugs" more like this: > 1. Suppose we have a document with version 57 > 2. A bulk of delete and reindex will remove the index-v57, increase the version to 58 (for the delete operation), then put a new doc with version 59. While the engine places the index-59 into the version map, the safe-access flag is flipped over (due to a concurrent fresh), the engine won't put that index entry into the version map, but also leave the delete-58 tombstone in the version map. The delete-58 tombstone is stale because the latest version of that document is index-59. > 3. Another bulk of delete and reindex will increase the version to 59 (for a delete) but won't remove docs from Lucene because of the existing (stale) delete-58 tombstone. The index operation will append document (version 60) to Lucene (instead of overwriting). At this point, we will have two documents with the same id. Which was a bug TLA+ found in ElasticSearch.[2] [1]: https://dl.acm.org/doi/10.5555/1779934.1779955 https://dl.acm.org/doi/10.5555/1779934.1779955 [2]: https://github.com/elastic/elasticsearch/issues/31976#issuecomment-404722753 https://github.com/elastic/elasticsearch/issues/31976#issuec...
candiodari 7y ago
TLA+: you mean the transitions of one variable are formally proven. Whilst a plus, this is not that different from how compilers were written since the 1980s. Never saw any crash happen there. You should think of these systems like you think of garbage collection. They lower (sometimes eliminate) one particular kind of problem, and that's it. It does not prove the code works, doesn't OOM, doesn't segfault, doesn't dos itself, doesn't enter infinite loop, etc.

zytek 7y ago

AWS S3, as far as I know

hwayne 7y ago
The design of S3 was formally specified, but not the actual code.

rurban 7y ago

I would count Simulink RT as formally sound and safe, because you can only wire matching boxes together. Graphically. It's the standard in Automotive, flight stuff also I heard.

0xffff2 7y ago
I do actually have a bit of Simulink generated code in my current project. I absolutely do not consider it to be formally anything. It's one of the highest risk areas of the project IMO because it is very complex and a very black box.
- magduf 7y ago
  I worked with a Simulink-generated system in a previous job. The generated code was absolutely unreadable by humans, and honestly downright ugly. I agree, it is very high-risk because it is a black box.
vsskanth 7y ago
I've used Simulink to model dynamic systems. I would say the C code it generates is "safe" in terms of memory access that can be used for embedded systems, but it does not check for undefined control behavior.
- rurban 7y ago
  I did not only use it, I generated a C++ compiler backend for it. Of course is generated code ugly, that's not the point. It's generated. Logical problems (and problems in C extensions) are of course always possible, therefore you have Stateflow and other methods. Other formal methods cannot guarantee that neither.

DoingIsLearning 7y ago

The Ada language allows for a subset of the language called SPARK (not to be confused with the Java framework). In Ada you can do Design-by-contract but in the SPARK subset you can actually formally prove the implementation's correctness. SPARK is used to my knowledge in rail signalling system, air traffic control systems, Class III medical devices, and now also NVDIA plans to use it for sections of their ADAS platform. I think the cost aspect is overblown. The biggest issue is that anything related to Ada is not really that well known and often what is known is based on stereotypes from the 80's. Also for most people they would not see it as career growth move to switch to an Ada based technology stack.

hwayne 7y ago

seL4 comes to mind. Also IronFleet[1], which is small but end-to-end verified in Dafny. People tend to verify the cores of complex systems, not the entire thing. See here[2] for more on that. I suspect there'd be a lot of stuff using either SPARK or Event-B, but Tokeneer[3] is the only thing I found with five minutes of Googling. [1]: https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle... [2]: https://www.cs.purdue.edu/homes/pfonseca//papers/eurosys2017-dsbugs.pdf https://www.cs.purdue.edu/homes/pfonseca//papers/eurosys2017... [3]: https://www.adacore.com/tokeneer https://www.adacore.com/tokeneer