3 ms·

SPARK is indeed very adapted to some kinds of code (protocols, serialization, deserialization, index manipulation, masks...). Proving the absence of runtime err

SPARK is indeed very adapted to some kinds of code (protocols, serialization, deserialization, index manipulation, masks...). Proving the absence of runtime errors in such code is easy (not much help needed for the provers, just type your data structures well) and makes you think of every case. Fun. Even better : once AoRTE is proved, remove all runtime checks and get C-like performance. You can also prove some isolated functional properties ('the answer to message X can only be message Y or Z'... just sprinkle some asserts, post-conditions or check the nice Contract_Case syntax). Or you can go to 'platinum'-level and prove your complete protocol/algorithm. The tech is great and it keeps improving, it gets easier every year...

nickpsecurity 10y ago
Oh yeah, Rod Chapman and others at Praxis did amazing work. It's probably the single, most-practical tools in engineered software since abstract, state machines for specification or Cleanroom for building. Their error rate was so low. The traditional problem, though, was that some tools were good for specifying full correctness of high-level models while others were good for verifying properties of code itself. They rarely did both well. Still true with SPARK. Before DeepSpec, I was already pushing for mixing them up a lot with different tools on different components with some sort of unified logic. You might find it interesting that one of those was with SPARK and the successful Event-B method. I'll give you a paper show how hard it is to use Event-B by itself down to low-level code followed by how a combo improves things. http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 One last thing before I head out is that the landing system paper is great for illustrating difficulty of correctness. It shows a small number of straight-forward requirements and design specs. Then, verification conditions are derived down to the low level code that must all be maintained true for total correctness. As in, it makes explicit all the stuff a developer must get right in their head to correctly solve this simple problem. I find it's a nice reality check for people even if they don't know the notation on intrinsic complexity of software & how that affects verification. Especially why you want to use simpler, automated methods than hope to test your way out of that level of complexity w/ corner cases. ;)
- touisteur 10y ago
  Thanks for the paper. It's indeed a game-changer to be able to mix Ada2012, Spark, and C in an industry-grade programming environment. You can gradually convert a legacy codebase. I've been replacing some crufty C parts with Ada-with-Spark-restrictions then full-Spark-with-AoRTE-proof and even some functional proof with great success and can now stop worrying about crashes in security-sensitive attack-surface parts. Network/file interfaces, etc. Most of my experiments are very encouraging ! Coupled with CodePeer and/or afl-fuzz for Ada code, almost-bug-free code becomes somewhat more accessible. Rod Chapman is also a great showman with great success stories, also very funny... and Yannick Moy at AdaCore is an amazing teacher and doing great work leading Spark further, including on small embedded targets. I think you're doing great work around here reminding everyone once in a while about Ada & Spark, especially in articles that devolve into 'Rust-would-have-caught-it' :-).
  - nickpsecurity 10y ago
    Appreciate the kind words. I plan to get back to experimenting myself. One of my ideas is coding in both Rust and Ada/SPARK to let borrow checker catch temporal errors while Ada/SPARK handles the rest. Optionally a C version or use an Ada-to-C compiler if Taft's is still available to throw every free analyzer or tester for C at it. Far as apps, check out Ironsides DNS that was done in SPARK. Borrow-checking and testing it will be my first project if it get back into Ada. Note: There's also work right now on a verified front-end for SPARK to integrate it into CompCert. Then, the ASM is verified as well. Exciting times. :) EDIT to add: Yeah, that Rust would've caught it was a bit annoying. Worst was them saying it was first, safe, systems language. pjmpl and I demolished that one, though. Now we just get the other one which is at least accurate if it's memory bugs. Progress. (Shrugs)
    - touisteur 10y ago
      Well then you're going to be happy : there's a new Spark-to-C compiler. http://blog.adacore.com/spark-tetris-on-the-arduboy http://blog.adacore.com/spark-tetris-on-the-arduboy Maybe that's the one you're thinking about ? Also, I heard Rod Chapman (at the last AdaCore tech day) say they had great success using 'the' Ada-to-C compiler some years ago. Looks like AdaCore still have the code for it, not doing much with it. You might get the code if you ask nicely (maybe T.Taft directly now that he works for AdaCore) :-D. If you get any new idea on some combination of Spark, Ada and other tech, I'd send yannick moy an email :-D. Always helpful and insightful. If you plan on doing your borrow checker as some kind of new static analysis pass for Ada, I'd also look into libadalang, there's some great (open source !) progress there. I also played a lot with gnat2xml but I don't recommend : it works but it was painful... I also wondered some time ago about a Spark-to-rust compiler. But I'm waiting for my rust skills to improve first. Anyway, it's very strange to see rust every so often mentionned for embedded software. I get the interest for 'normal' unconstrained software. But after 10 years of large-scale real-time embedded-systems programming in Ada and I maybe faced once a memory safety bug that the borrow checker would have prevented. Mostly the bugs you get are constraint_errors (overflow, underflow, array bounds,...) most already caught by the type system at compile or static-analysis time. The rest are mostly 'real' bugs : logic or temporal. You never doubt of the state of the program when reading the code, such a lower cognitive load... Going back to C from time to time is so painful, especially, when you think of all the help you're missing. When in need of pointer go for not null access types, when in need for dynamic allocation go for controlled types (scoped deallocation) and storage pools... Everyone (except haskellers...) is missing on so much, it feels like living in the future where the compiler works (a lot !) for you. Sorry for the rant... By the way I found one of the ways to catch temporal errors (other than uninitialized variables that are caught) in Spark is to use an enumerated state variable and check it all the time (post/pre or in invariants). It's almost always a good idea anyway to have an explicit state instead of some 'nah none will call this code in such sequence...'. Also interesting : like functional programming or the borrow checker, or strong typing, Spark changes the way you think about your code. You think about how 'provable' your design and code is and it makes code more readable, simple. You can also just start with data flow annotations (also great for safety and security-critical code), makes reading code easier. I'll be looking out for your next dive back into Ada then !

nickpsecurity 10y ago

Oh yeah, Rod Chapman and others at Praxis did amazing work. It's probably the single, most-practical tools in engineered software since abstract, state machines for specification or Cleanroom for building. Their error rate was so low. The traditional problem, though, was that some tools were good for specifying full correctness of high-level models while others were good for verifying properties of code itself. They rarely did both well. Still true with SPARK. Before DeepSpec, I was already pushing for mixing them up a lot with different tools on different components with some sort of unified logic. You might find it interesting that one of those was with SPARK and the successful Event-B method. I'll give you a paper show how hard it is to use Event-B by itself down to low-level code followed by how a combo improves things. http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 http://journal.ub.tu-berlin.de/eceasst/article/view/785/782 One last thing before I head out is that the landing system paper is great for illustrating difficulty of correctness. It shows a small number of straight-forward requirements and design specs. Then, verification conditions are derived down to the low level code that must all be maintained true for total correctness. As in, it makes explicit all the stuff a developer must get right in their head to correctly solve this simple problem. I find it's a nice reality check for people even if they don't know the notation on intrinsic complexity of software & how that affects verification. Especially why you want to use simpler, automated methods than hope to test your way out of that level of complexity w/ corner cases. ;)

touisteur 10y ago
Thanks for the paper. It's indeed a game-changer to be able to mix Ada2012, Spark, and C in an industry-grade programming environment. You can gradually convert a legacy codebase. I've been replacing some crufty C parts with Ada-with-Spark-restrictions then full-Spark-with-AoRTE-proof and even some functional proof with great success and can now stop worrying about crashes in security-sensitive attack-surface parts. Network/file interfaces, etc. Most of my experiments are very encouraging ! Coupled with CodePeer and/or afl-fuzz for Ada code, almost-bug-free code becomes somewhat more accessible. Rod Chapman is also a great showman with great success stories, also very funny... and Yannick Moy at AdaCore is an amazing teacher and doing great work leading Spark further, including on small embedded targets. I think you're doing great work around here reminding everyone once in a while about Ada & Spark, especially in articles that devolve into 'Rust-would-have-caught-it' :-).
- nickpsecurity 10y ago
  Appreciate the kind words. I plan to get back to experimenting myself. One of my ideas is coding in both Rust and Ada/SPARK to let borrow checker catch temporal errors while Ada/SPARK handles the rest. Optionally a C version or use an Ada-to-C compiler if Taft's is still available to throw every free analyzer or tester for C at it. Far as apps, check out Ironsides DNS that was done in SPARK. Borrow-checking and testing it will be my first project if it get back into Ada. Note: There's also work right now on a verified front-end for SPARK to integrate it into CompCert. Then, the ASM is verified as well. Exciting times. :) EDIT to add: Yeah, that Rust would've caught it was a bit annoying. Worst was them saying it was first, safe, systems language. pjmpl and I demolished that one, though. Now we just get the other one which is at least accurate if it's memory bugs. Progress. (Shrugs)
  - touisteur 10y ago
    Well then you're going to be happy : there's a new Spark-to-C compiler. http://blog.adacore.com/spark-tetris-on-the-arduboy http://blog.adacore.com/spark-tetris-on-the-arduboy Maybe that's the one you're thinking about ? Also, I heard Rod Chapman (at the last AdaCore tech day) say they had great success using 'the' Ada-to-C compiler some years ago. Looks like AdaCore still have the code for it, not doing much with it. You might get the code if you ask nicely (maybe T.Taft directly now that he works for AdaCore) :-D. If you get any new idea on some combination of Spark, Ada and other tech, I'd send yannick moy an email :-D. Always helpful and insightful. If you plan on doing your borrow checker as some kind of new static analysis pass for Ada, I'd also look into libadalang, there's some great (open source !) progress there. I also played a lot with gnat2xml but I don't recommend : it works but it was painful... I also wondered some time ago about a Spark-to-rust compiler. But I'm waiting for my rust skills to improve first. Anyway, it's very strange to see rust every so often mentionned for embedded software. I get the interest for 'normal' unconstrained software. But after 10 years of large-scale real-time embedded-systems programming in Ada and I maybe faced once a memory safety bug that the borrow checker would have prevented. Mostly the bugs you get are constraint_errors (overflow, underflow, array bounds,...) most already caught by the type system at compile or static-analysis time. The rest are mostly 'real' bugs : logic or temporal. You never doubt of the state of the program when reading the code, such a lower cognitive load... Going back to C from time to time is so painful, especially, when you think of all the help you're missing. When in need of pointer go for not null access types, when in need for dynamic allocation go for controlled types (scoped deallocation) and storage pools... Everyone (except haskellers...) is missing on so much, it feels like living in the future where the compiler works (a lot !) for you. Sorry for the rant... By the way I found one of the ways to catch temporal errors (other than uninitialized variables that are caught) in Spark is to use an enumerated state variable and check it all the time (post/pre or in invariants). It's almost always a good idea anyway to have an explicit state instead of some 'nah none will call this code in such sequence...'. Also interesting : like functional programming or the borrow checker, or strong typing, Spark changes the way you think about your code. You think about how 'provable' your design and code is and it makes code more readable, simple. You can also just start with data flow annotations (also great for safety and security-critical code), makes reading code easier. I'll be looking out for your next dive back into Ada then !