6 ms·

Safe Pointers in SPARK 2014

70 points by touisteur 9y ago

stmw 9y ago
You know Rust is gaining traction when people are writing papers discussing adding Rust borrow-checker features to an Ada-inspired safe languages!
- pjmlp 9y ago
  The biggest impact was definitely to make more approachable the design of ATS and Cyclone to common developers. But borrow-checker still needs some fine tuning, as per NLL and further planned work.
- cwzwarich 9y ago
  To be honest, the system in this paper doesn't really match the Rust system at all. It isn't based on regions and all borrows occur upon function calls, so it's pretty similar to pre-Cyclone alias-tracking features. For embedded Ada programs, this simpler form is probably sufficient. The main improvement you'd get from Cyclone-style nested regions is being able to type-check functions that produce outputs that are themselves borrowed pointers, either by returning them or storing them in a data structure passed as an argument. In embedded code you're much less likely to have dynamic data structures whose lifetimes are anchored to a given stack frame or control-flow region, so this isn't as useful as it is for the C++11ish coding style encouraged by Rust.
- Volt 9y ago
  You know Lisp is gaining traction when…
  - wtallis 9y ago
    Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust. By contrast, when a modern language adopts something from Lisp, that doesn't really say anything new about Lisp. It's been around forever and everyone who actually bothers to learn about the history of programming languages knows Lisp has a lot to teach those who bother to learn. When a new language borrows from Lisp, that says more about the state of the new language author's education than about Lisp itself.
    - Raphael_Amiard 9y ago
      > Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust. It definitely does ! And FWIW I work at AdaCore, and even though Rust did not invent those features, I can safely say that the work we do on safe pointer is very directly inspired by Rust. So kudos to Rust :)
    - kazinator 9y ago
      > When a new language borrows from Lisp, that says more about the state of the new language author's education than about Lisp itself. Namely that that education, while it has some merit, is incomplete. Otherwise, of course, that language would be a Lisp.
silverlake 9y ago
Why don’t more people use SPARK?
- MisterTea 9y ago
  Why don't more people use Ada?
  - nickpsecurity 9y ago
    Anyone curious of its benefits can find them here: https://www.adacore.com/books/safe-and-secure-software https://www.adacore.com/books/safe-and-secure-software Throw in a good article on top: http://www.electronicdesign.com/embedded-revolution/assessing-ada-language-audio-applications http://www.electronicdesign.com/embedded-revolution/assessin...
  - yeukhon 9y ago
    Ada is quite common in aircraft system programming. P.S. I thought I read SPARC.
    - Lucretia9000 9y ago
      Yes but embedded / safety programming isn't the only programming. Ada could very well be used in all areas.
      - pjmlp 9y ago
        Ada only caters to developers and industries that care about quality before price, and where sloppy programming and cutting corners might kill people. Given that the computer industry still enjoys EULAs with disclaimers, product refunds and lawsuits due to sloppy programming or CVE exploits are still pretty rare, it is almost impossible to convince people otherwise. One of the great outcomes of the increase in malware attacks is finally getting more buy-in for safer native languages.
- th0br0 9y ago
  Because of licensing?
kuwze 9y ago
There is also safe_ptr[0] in case anyone is interested. [0]: http://archive.adaic.com/intro/tech/safe_ptr.html http://archive.adaic.com/intro/tech/safe_ptr.html
- pjmlp 9y ago
  Thanks, quite interesting, specially the publication year (1999), yet another proof how long people have been trying to advocate for safer systems.
nickpsecurity 9y ago
I told Yannick at AdaCore that getting parity with Rust's borrow-checker was critical given SPARK was otherwise the champ of highly-assured, system code. He said someone was working on something like that. I appreciate the tip from touisteur about this work because it's awesome! This is also potentially a boost for my Brute-Force Assurance concept of doing versions of same code in multiple languages to leverage their verification tooling, esp automated. One obstacle was mismatch between Rust's pointers with borrow-checker and SPARK's lack of them. Bringing them closer together might let one use SPARK to model unsafe code in Rust to prove its safety. Other languages, too.
- touisteur 9y ago
  By the way, slightly off-topic but I found an interesting thread that might get you some answers about the state of the art on automatic proof of floating point operations (our last conversation on the subject) : http://lists.forge.open-do.org/pipermail/spark2014-discuss/2017-November/001444.html http://lists.forge.open-do.org/pipermail/spark2014-discuss/2... Lots of links to recent stuff, you should look it all... If you have the time :-D.
- adrianN 9y ago
  Modelling Rust's unsafe code seems pretty hard to me as afaik there are no formal semantics for Rust.
  - nickpsecurity 9y ago
    In that case, one could just go with the semantics of the SPARK-like tool with equivalent algorithm, turn that to C or assembly, and use it with Rust's FFI. That's similar to my proposal for Rust + x86 Proved or TALC. This is also an area where formal specifications can have benefit showing intent for unsafe Rust and the proven replacement.
  - touisteur 9y ago
    I guess people will try anyway : https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... There's some great work on this front coming from the Rustbelt lab : https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf and http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/
deleted 9y ago
[deleted]
awirth 9y ago
This is a really cool paper with impressive results. An interesting property that this paper doesn't consider (I believe the language described does not allow it though) is casting pointers/references to integers. Many languages consider this unsafe, but Rust does not. Considering casting pointers to integers unsafe prevents 'address disclosure' vulnerabilities, which is relevant in the context of any program that incorporates (potentially buggy) unsafe code (read: all of them). This can be used to defeat ASLR.
- Lucretia9000 9y ago
  Ada.Unchecked_Conversion?
  - touisteur 9y ago
    More like the safer : http://www.adaic.org/resources/add_content/standards/05rm/html/RM-13-7-2.html http://www.adaic.org/resources/add_content/standards/05rm/ht... ? And to display addresses (with GNAT only...) : https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-addima__ads.htm https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-add... . Nothing preventing you to display addresses anyway. Surely something I've reached only once or twice in 10+ years of Ada. I'm left wondering how one could debug low-level stuff without it. Sure you can use gdb, valgrind. But sometimes you can't. You can probably make this a coding rule and find something to check it in Gnatcheck (http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gnatcheck_rm/predefined_rules.html#unchecked-address-conversions http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gna...) or AdaControl (http://www.adalog.fr/en/AdaControl.html http://www.adalog.fr/en/AdaControl.html). Something you can do with ASIS (https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Specification https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Speci...) or libadalang (http://blog.adacore.com/introducing-libadalang http://blog.adacore.com/introducing-libadalang) is to build your own linter to check the use of this kind of operations. For the curious about pointers in Ada (it is sometimes a bit confusing if you're coming from the pointer-is-an-integer-like-an-other-right? crowd, as I once was) : https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access. It barely scrapes the surface but for a nicer introduction I can only recommend the 'Barnes' (http://www.cambridge.org/fr/academic/subjects/computer-science/software-engineering-and-development/programming-ada-2012?format=PB&isbn=9781107424814 http://www.cambridge.org/fr/academic/subjects/computer-scien...) in dead-tree form or a gentle introduction by JP Rosen at FOSDEM 2016 (pdf) : https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/16/160130-fosdem/09-ada-memory.pdf https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/ev...
deleted 9y ago
[deleted]
dwheeler 9y ago
This is really impressive work. Formally proving programs correct is especially hard when there are pointers. This approach manages to handle them, without even requiring special programmer annotations like Rust requires. I'm a big fan of the Why3 / ProVal / Toccata approach. Instead of building one tool to do everything, they've broken things down so they can support multiple programming languages (C / Java / Ada / Why's ML variant), multiple automated provers (e.g., Z3, alt-ergo), and multiple interactive provers (Coq, Isabelle). It seems to be a very promising approach. Cool! Thanks for sharing!
- andrewflnr 9y ago
  You can't mention something like that without a link! http://why3.lri.fr http://why3.lri.fr
deleted 9y ago
[deleted]

70 points by touisteur 9y ago

stmw 9y ago

You know Rust is gaining traction when people are writing papers discussing adding Rust borrow-checker features to an Ada-inspired safe languages!

pjmlp 9y ago
The biggest impact was definitely to make more approachable the design of ATS and Cyclone to common developers. But borrow-checker still needs some fine tuning, as per NLL and further planned work.
cwzwarich 9y ago
To be honest, the system in this paper doesn't really match the Rust system at all. It isn't based on regions and all borrows occur upon function calls, so it's pretty similar to pre-Cyclone alias-tracking features. For embedded Ada programs, this simpler form is probably sufficient. The main improvement you'd get from Cyclone-style nested regions is being able to type-check functions that produce outputs that are themselves borrowed pointers, either by returning them or storing them in a data structure passed as an argument. In embedded code you're much less likely to have dynamic data structures whose lifetimes are anchored to a given stack frame or control-flow region, so this isn't as useful as it is for the C++11ish coding style encouraged by Rust.
Volt 9y ago
You know Lisp is gaining traction when…
- wtallis 9y ago
  Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust. By contrast, when a modern language adopts something from Lisp, that doesn't really say anything new about Lisp. It's been around forever and everyone who actually bothers to learn about the history of programming languages knows Lisp has a lot to teach those who bother to learn. When a new language borrows from Lisp, that says more about the state of the new language author's education than about Lisp itself.
  - Raphael_Amiard 9y ago
    > Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust. It definitely does ! And FWIW I work at AdaCore, and even though Rust did not invent those features, I can safely say that the work we do on safe pointer is very directly inspired by Rust. So kudos to Rust :)
  - kazinator 9y ago
    > When a new language borrows from Lisp, that says more about the state of the new language author's education than about Lisp itself. Namely that that education, while it has some merit, is incomplete. Otherwise, of course, that language would be a Lisp.

silverlake 9y ago

Why don’t more people use SPARK?

MisterTea 9y ago
Why don't more people use Ada?
- nickpsecurity 9y ago
  Anyone curious of its benefits can find them here: https://www.adacore.com/books/safe-and-secure-software https://www.adacore.com/books/safe-and-secure-software Throw in a good article on top: http://www.electronicdesign.com/embedded-revolution/assessing-ada-language-audio-applications http://www.electronicdesign.com/embedded-revolution/assessin...
- yeukhon 9y ago
  Ada is quite common in aircraft system programming. P.S. I thought I read SPARC.
  - Lucretia9000 9y ago
    Yes but embedded / safety programming isn't the only programming. Ada could very well be used in all areas.
    - pjmlp 9y ago
      Ada only caters to developers and industries that care about quality before price, and where sloppy programming and cutting corners might kill people. Given that the computer industry still enjoys EULAs with disclaimers, product refunds and lawsuits due to sloppy programming or CVE exploits are still pretty rare, it is almost impossible to convince people otherwise. One of the great outcomes of the increase in malware attacks is finally getting more buy-in for safer native languages.
th0br0 9y ago
Because of licensing?

kuwze 9y ago

There is also safe_ptr[0] in case anyone is interested. [0]: http://archive.adaic.com/intro/tech/safe_ptr.html http://archive.adaic.com/intro/tech/safe_ptr.html

pjmlp 9y ago
Thanks, quite interesting, specially the publication year (1999), yet another proof how long people have been trying to advocate for safer systems.

nickpsecurity 9y ago

I told Yannick at AdaCore that getting parity with Rust's borrow-checker was critical given SPARK was otherwise the champ of highly-assured, system code. He said someone was working on something like that. I appreciate the tip from touisteur about this work because it's awesome! This is also potentially a boost for my Brute-Force Assurance concept of doing versions of same code in multiple languages to leverage their verification tooling, esp automated. One obstacle was mismatch between Rust's pointers with borrow-checker and SPARK's lack of them. Bringing them closer together might let one use SPARK to model unsafe code in Rust to prove its safety. Other languages, too.

touisteur 9y ago
By the way, slightly off-topic but I found an interesting thread that might get you some answers about the state of the art on automatic proof of floating point operations (our last conversation on the subject) : http://lists.forge.open-do.org/pipermail/spark2014-discuss/2017-November/001444.html http://lists.forge.open-do.org/pipermail/spark2014-discuss/2... Lots of links to recent stuff, you should look it all... If you have the time :-D.
adrianN 9y ago
Modelling Rust's unsafe code seems pretty hard to me as afaik there are no formal semantics for Rust.
- nickpsecurity 9y ago
  In that case, one could just go with the semantics of the SPARK-like tool with equivalent algorithm, turn that to C or assembly, and use it with Rust's FFI. That's similar to my proposal for Rust + x86 Proved or TALC. This is also an area where formal specifications can have benefit showing intent for unsafe Rust and the proven replacement.
- touisteur 9y ago
  I guess people will try anyway : https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html https://kha.github.io/2016/07/22/formally-verifying-rusts-bi... There's some great work on this front coming from the Rustbelt lab : https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf and http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/

deleted 9y ago

[deleted]

awirth 9y ago

This is a really cool paper with impressive results. An interesting property that this paper doesn't consider (I believe the language described does not allow it though) is casting pointers/references to integers. Many languages consider this unsafe, but Rust does not. Considering casting pointers to integers unsafe prevents 'address disclosure' vulnerabilities, which is relevant in the context of any program that incorporates (potentially buggy) unsafe code (read: all of them). This can be used to defeat ASLR.

Lucretia9000 9y ago
Ada.Unchecked_Conversion?
- touisteur 9y ago
  More like the safer : http://www.adaic.org/resources/add_content/standards/05rm/html/RM-13-7-2.html http://www.adaic.org/resources/add_content/standards/05rm/ht... ? And to display addresses (with GNAT only...) : https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-addima__ads.htm https://www2.adacore.com/gap-static/GNAT_Book/html/rts/s-add... . Nothing preventing you to display addresses anyway. Surely something I've reached only once or twice in 10+ years of Ada. I'm left wondering how one could debug low-level stuff without it. Sure you can use gdb, valgrind. But sometimes you can't. You can probably make this a coding rule and find something to check it in Gnatcheck (http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gnatcheck_rm/predefined_rules.html#unchecked-address-conversions http://docs.adacore.com/live/wave/asis/html/gnatcheck_rm/gna...) or AdaControl (http://www.adalog.fr/en/AdaControl.html http://www.adalog.fr/en/AdaControl.html). Something you can do with ASIS (https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Specification https://en.m.wikipedia.org/wiki/Ada_Semantic_Interface_Speci...) or libadalang (http://blog.adacore.com/introducing-libadalang http://blog.adacore.com/introducing-libadalang) is to build your own linter to check the use of this kind of operations. For the curious about pointers in Ada (it is sometimes a bit confusing if you're coming from the pointer-is-an-integer-like-an-other-right? crowd, as I once was) : https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access https://en.m.wikibooks.org/wiki/Ada_Programming/Types/access. It barely scrapes the surface but for a nicer introduction I can only recommend the 'Barnes' (http://www.cambridge.org/fr/academic/subjects/computer-science/software-engineering-and-development/programming-ada-2012?format=PB&isbn=9781107424814 http://www.cambridge.org/fr/academic/subjects/computer-scien...) in dead-tree form or a gentle introduction by JP Rosen at FOSDEM 2016 (pdf) : https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/events/16/160130-fosdem/09-ada-memory.pdf https://people.cs.kuleuven.be/~dirk.craeynest/ada-belgium/ev...

deleted 9y ago

[deleted]

dwheeler 9y ago

This is really impressive work. Formally proving programs correct is especially hard when there are pointers. This approach manages to handle them, without even requiring special programmer annotations like Rust requires. I'm a big fan of the Why3 / ProVal / Toccata approach. Instead of building one tool to do everything, they've broken things down so they can support multiple programming languages (C / Java / Ada / Why's ML variant), multiple automated provers (e.g., Z3, alt-ergo), and multiple interactive provers (Coq, Isabelle). It seems to be a very promising approach. Cool! Thanks for sharing!

andrewflnr 9y ago
You can't mention something like that without a link! http://why3.lri.fr http://why3.lri.fr

deleted 9y ago

[deleted]