Putting this here for the next time "someone" asks the misguided question "why don't you use formal methods to develop Linux": https://web.archive.org/web/20140630071239/http://www.cypherpunks.to/~peter/04_verif_techniques.pdf … Personally, I like to think we have learned from past mistakes...
For some things, where you can actually write a specification that is accurate, it can work. But look at the effort it takes, and again, the lack of ability to do that for almost all hardware, which is what a kernel cares about.
-
-
And that AWS work is wonderful to see happen, any work like this for well-defined mission-critical code is better than not doing it. The very act of writing the spec is what usually fixes the code up, that has long been proven. But again, remember, hardware sucks :)
-
Yes, it is the rigor required to write the spec that often flushes out the errors. And when you have trust chaining of "secure boot" type systems, starting as close to the bottom turtle as you can is probably a good idea. http://www.kroening.com/papers/cav2018-aws.pdf …
- Pokaż odpowiedzi
Nowa rozmowa -
Wydaje się, że ładowanie zajmuje dużo czasu.
Twitter jest przeciążony lub wystąpił chwilowy problem. Spróbuj ponownie lub sprawdź status Twittera, aby uzyskać więcej informacji.
