6 ms·

naive question, but shouldn't AV command and control algorithms be built on some kind of formally verified system/language, considering lives are at play here ?

naive question, but shouldn't AV command and control algorithms be built on some kind of formally verified system/language, considering lives are at play here ? I am aware of MISRA C for automotive but is something like that sufficient to guarantee against unintended behavior ? If not, can someone comment on why this isn't the case today ?

pjc50 7y ago
There's a huge amount of money riding on the assumption that with enough training the neural net solutions will have an error rate low enough that the "Explain why the crash is the other person's fault" PR division can cover for it.
0xffff2 7y ago
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
jeffreyrogers 7y ago
I've looked into formal verification in the past and from what I've seen it boils down to either annotating your source code with constraints that are then checked to verify the software does what you say it does, or you write a specification in a separate language that is supposed to represent the intended functionality of the system and then you write the system such that it matches the specification. The problem in both these cases is that "formally verified" just means that you verify your specification doesn't violate anything you've said it shouldn't, but you might have written your specification incorrectly, or your specification might not match what you say it matches, which then makes the whole thing irrelevant. That's not to say there's no value in formal verification, but I tend to see the value more in verifying some tricky protocol or very concurrent thing works properly (because these often have subtle bugs that are very hard to detect from inspection), rather than as a way to verify that your whole system works. Plus for autopilot, how would you even specify that? The problem is too big and ill-defined to be specified in any way that would be amenable to verification. Of course, individual sub-problems could be verified but that's no guarantee that the system as a whole works.
- vsskanth 7y ago
  is it not possible to specify global constraints and verify the code against that ? (ex. minimum 2 sensors should give an estimate of each attribute, vehicle should not be able to crash into anything, hierarchical control modes for sensor failure, etc.)
  - jeffreyrogers 7y ago
    You can definitely do the first of those examples and probably the last of the examples, but the middle one (vehicle should not be able to crash into anything) is really hard. How do you prove the vehicle can't crash into anything? What do you specify in code to ensure that? I guarantee whatever specification you make I can come up with an edge case that it won't handle. That's the main problem with specification, not that it doesn't work, but that we don't know enough about what a solution would look like to fully specify it. And just to dive into this a little more, let's say the first example you gave fails, and we have one sensor saying something is 10m in front of us and the other saying there's nothing for 100m, what do we do in this situation? Well, it depends on the context, maybe the one sensor is picking up a bit of retread tire in the middle of the lane and we can just drive over it, or maybe the other sensor is malfunctioning and there's actually a bear in the road. I don't think there is an easy answer to what to do in general just given the sensor state.
cpeterso 7y ago
I'm disappointed Tesla's safety-critical driving systems are developed using C/C++ instead of a safe language like SPARK Ada. I hear SpaceX also uses C++ for onboard ship software.
- vsskanth 7y ago
  I can understand there are compatibility issues at play wrt embedded systems, but aren't there ways to formally verify C/C++ code ?
- magduf 7y ago
  Good luck finding any software engineers who are proficient in Ada, much less a variant of it. I mean, they're out there: according to the SPARK Wikipedia page, it's been used in things like some Rolls-Royce jet engines, some military planes, some air traffic control applications, a cubesat project, etc. But there's orders of magnitude more engineers out there proficient in C and/or C++, plus even if you're willing to train, it's not that easy to find engineers willing to move into something that doesn't have broad industry support and might therefore limit their future career moves. C and C++ are already both used for safety-critical systems. MISRA C is the standard in automotive, and there's civilian (DO-178C) and military standards for C++.
josefx 7y ago
The only guarantee we most likely have is that you can hard kill it with an off switch or possibly by hitting the brakes. The higher steering logic runs on ML anyway and I don't see a way to formally verify the behavior of an algorithm trained on a set of one billion road pictures.

pjc50 7y ago

There's a huge amount of money riding on the assumption that with enough training the neural net solutions will have an error rate low enough that the "Explain why the crash is the other person's fault" PR division can cover for it.

0xffff2 7y ago

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

jeffreyrogers 7y ago

I've looked into formal verification in the past and from what I've seen it boils down to either annotating your source code with constraints that are then checked to verify the software does what you say it does, or you write a specification in a separate language that is supposed to represent the intended functionality of the system and then you write the system such that it matches the specification. The problem in both these cases is that "formally verified" just means that you verify your specification doesn't violate anything you've said it shouldn't, but you might have written your specification incorrectly, or your specification might not match what you say it matches, which then makes the whole thing irrelevant. That's not to say there's no value in formal verification, but I tend to see the value more in verifying some tricky protocol or very concurrent thing works properly (because these often have subtle bugs that are very hard to detect from inspection), rather than as a way to verify that your whole system works. Plus for autopilot, how would you even specify that? The problem is too big and ill-defined to be specified in any way that would be amenable to verification. Of course, individual sub-problems could be verified but that's no guarantee that the system as a whole works.

vsskanth 7y ago
is it not possible to specify global constraints and verify the code against that ? (ex. minimum 2 sensors should give an estimate of each attribute, vehicle should not be able to crash into anything, hierarchical control modes for sensor failure, etc.)
- jeffreyrogers 7y ago
  You can definitely do the first of those examples and probably the last of the examples, but the middle one (vehicle should not be able to crash into anything) is really hard. How do you prove the vehicle can't crash into anything? What do you specify in code to ensure that? I guarantee whatever specification you make I can come up with an edge case that it won't handle. That's the main problem with specification, not that it doesn't work, but that we don't know enough about what a solution would look like to fully specify it. And just to dive into this a little more, let's say the first example you gave fails, and we have one sensor saying something is 10m in front of us and the other saying there's nothing for 100m, what do we do in this situation? Well, it depends on the context, maybe the one sensor is picking up a bit of retread tire in the middle of the lane and we can just drive over it, or maybe the other sensor is malfunctioning and there's actually a bear in the road. I don't think there is an easy answer to what to do in general just given the sensor state.

cpeterso 7y ago

I'm disappointed Tesla's safety-critical driving systems are developed using C/C++ instead of a safe language like SPARK Ada. I hear SpaceX also uses C++ for onboard ship software.

vsskanth 7y ago
I can understand there are compatibility issues at play wrt embedded systems, but aren't there ways to formally verify C/C++ code ?
magduf 7y ago
Good luck finding any software engineers who are proficient in Ada, much less a variant of it. I mean, they're out there: according to the SPARK Wikipedia page, it's been used in things like some Rolls-Royce jet engines, some military planes, some air traffic control applications, a cubesat project, etc. But there's orders of magnitude more engineers out there proficient in C and/or C++, plus even if you're willing to train, it's not that easy to find engineers willing to move into something that doesn't have broad industry support and might therefore limit their future career moves. C and C++ are already both used for safety-critical systems. MISRA C is the standard in automotive, and there's civilian (DO-178C) and military standards for C++.

josefx 7y ago

The only guarantee we most likely have is that you can hard kill it with an off switch or possibly by hitting the brakes. The higher steering logic runs on ML anyway and I don't see a way to formally verify the behavior of an algorithm trained on a set of one billion road pictures.