4 ms·

Ada's formal verification capabilities have fallen behind Frama-C for ANSI/ISO C. Frama-C allows formal verification of essentially arbitrary heap manipulation

Ada's formal verification capabilities have fallen behind Frama-C for ANSI/ISO C. Frama-C allows formal verification of essentially arbitrary heap manipulation algorithms. You can implement linked lists and graphs in traditional C with Frama-C annotations in the comments, then prove your code never dereferences NULL, never has an integer overflow, etc. One single commercial Ada vendor offers Spark, a formally verifiable subset of Ada. Spark does not allow arbitrary dynamically allocated data structures like Frama-C does. https://frama-c.com/ https://frama-c.com/

p_l 5y ago
Seems that's no longer true, as current SPARK version permits pointers given they follow certain memory ownership policy.
- dandotway 5y ago
  Yes, SPARK has a Rust-like borrow checker that doesn't allow implementing arbitrary pointer graphs. You have to use 'unsafe Rust' to implement linked list containers which, once implemented, other parts of the codebase can then consume in 'safe Rust'. Seems to be the same deal with SPARK ('safe Ada') vs vanilla Ada ('unsafe Ada').
  - p_l 5y ago
    Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
    - dandotway 5y ago
      The SPARK example I found uses singly-linked lists and says doubly-linked lists and graphs with cycles are not supported: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)
rurban 5y ago
With CBMC it's even easier. You don't need magic comments in foreign languages to prove linked lists, arrays, graphs, trees, hashtables, ... If you need to formalize contracts you do it in C, but rarely need it http://www.cprover.org/cbmc/ http://www.cprover.org/cbmc/
touisteur 5y ago
Strange (but interesting (point of view. I always found Frama-C so verbose where spark has most checks as implicit, and has ways to express not-null pointer as types. I've always found eacsl a pain to write and even more with pointer manipulation. Spark has added checks on memory ownership, that it seems (willing to be corrected) Frama-C didn't have yet. From a pure tech stack point of view, down there you'll find Why3 and SMT solvers to perform most automatic proof/discharging of verification conditions, and then around that you'll find either a rich set of plugins (Frama-C) because C is... a tall order, or a series of static analysis tools (heavy-duty like codepeer, or lightweight libadalang-based abstract interpretation things) combined into the proof and verification environment. There's also been a lot of amazing work on floating point code verification for both in the previous years, and it was done mostly at the Why3 and SMT solver (or different kind of solvers/verifiers such as gappa) so everyone profits. And, lest people might think both communities don't interact, the Spark and Frama-C people have an annual (or is it every other year) joint conference. I'd be quite happy to find more people diving into Frama-C and see what they do and how they manage to write safe software. I'd also be quite happy to see rust building over Why3 (among other things) for their proof/verification efforts. More fruits from all the deep efforts of the verification community.
- dandotway 5y ago
  Responding to each point you raised: 'Frama-C so verbose': ??? Ada is the most verbose programming language, ever, even before you had the extremely verbose Spark contracts. Could you show me an example of Frama-C with annotations being more verbose than Ada/Spark? 'Spark has added checks on memory ownership': A Rust-like pointer ownership tester has its advantages and limitations. Advantages: if you have team of 20 engineers working on a 20 million line web browser and no single engineer understands how the whole code base works, a pointer borrow-checker prevents an important class of errors. Disadvantages: Rust tutorials point out that you have to resort to 'unsafe Rust' to implement even an intro-to-computer-science linked list. You have to use unsafe Rust to implement your fancy heap manipulation algorithms. Unsafe vs safe Rust is a bit like Ada vs. Spark ("safe Ada"). 'I'd be quite happy to find more people diving into Frama-C': Frama-C is trending upward and Ada is in decline, ever since the Ariane 5 explosion on 4 June 1996. The US DOD consequently shut down its Ada office and eliminated the Ada requirement, and C/C++ subsets increasingly dominated.
philwise 5y ago
Are there vendors who provide support for tool qualification for frama-c? By that I mean documentation support that can be provided as part of the certification process, so when you say "Frama-c verified this code does not contain any arithmetic overflow", it is possible to back that up with "And Frama-c version x.y.z has sound analysis, evidenced by ...."
- dandotway 5y ago
  Great question. C/C++ is definitely trending upward in 'safe software' systems even though it isn't ready and industry as a whole isn't (as far as I know) using Frama-C. Are Tesla/Google/Apple hiring Ada engineers to build the car autopilots that control whether we live or die? Nope, seems to all be C++, God help us all.

p_l 5y ago

Seems that's no longer true, as current SPARK version permits pointers given they follow certain memory ownership policy.

dandotway 5y ago
Yes, SPARK has a Rust-like borrow checker that doesn't allow implementing arbitrary pointer graphs. You have to use 'unsafe Rust' to implement linked list containers which, once implemented, other parts of the codebase can then consume in 'safe Rust'. Seems to be the same deal with SPARK ('safe Ada') vs vanilla Ada ('unsafe Ada').
- p_l 5y ago
  Interestingly both Frama-C and SPARK use linked list as an example. But yes, not everything can be verified, though I'd rather bet on Ada than Rust in this area.
  - dandotway 5y ago
    The SPARK example I found uses singly-linked lists and says doubly-linked lists and graphs with cycles are not supported: https://blog.adacore.com/pointer-based-data-structures-in-spark https://blog.adacore.com/pointer-based-data-structures-in-sp... Yes, I could and should have been more explicit when I spoke of 'linked lists' without further qualification. While talking about these languages designed to eliminate all ambiguity I would do well to be unambiguous. :-)

rurban 5y ago

With CBMC it's even easier. You don't need magic comments in foreign languages to prove linked lists, arrays, graphs, trees, hashtables, ... If you need to formalize contracts you do it in C, but rarely need it http://www.cprover.org/cbmc/ http://www.cprover.org/cbmc/

touisteur 5y ago

Strange (but interesting (point of view. I always found Frama-C so verbose where spark has most checks as implicit, and has ways to express not-null pointer as types. I've always found eacsl a pain to write and even more with pointer manipulation. Spark has added checks on memory ownership, that it seems (willing to be corrected) Frama-C didn't have yet. From a pure tech stack point of view, down there you'll find Why3 and SMT solvers to perform most automatic proof/discharging of verification conditions, and then around that you'll find either a rich set of plugins (Frama-C) because C is... a tall order, or a series of static analysis tools (heavy-duty like codepeer, or lightweight libadalang-based abstract interpretation things) combined into the proof and verification environment. There's also been a lot of amazing work on floating point code verification for both in the previous years, and it was done mostly at the Why3 and SMT solver (or different kind of solvers/verifiers such as gappa) so everyone profits. And, lest people might think both communities don't interact, the Spark and Frama-C people have an annual (or is it every other year) joint conference. I'd be quite happy to find more people diving into Frama-C and see what they do and how they manage to write safe software. I'd also be quite happy to see rust building over Why3 (among other things) for their proof/verification efforts. More fruits from all the deep efforts of the verification community.

dandotway 5y ago
Responding to each point you raised: 'Frama-C so verbose': ??? Ada is the most verbose programming language, ever, even before you had the extremely verbose Spark contracts. Could you show me an example of Frama-C with annotations being more verbose than Ada/Spark? 'Spark has added checks on memory ownership': A Rust-like pointer ownership tester has its advantages and limitations. Advantages: if you have team of 20 engineers working on a 20 million line web browser and no single engineer understands how the whole code base works, a pointer borrow-checker prevents an important class of errors. Disadvantages: Rust tutorials point out that you have to resort to 'unsafe Rust' to implement even an intro-to-computer-science linked list. You have to use unsafe Rust to implement your fancy heap manipulation algorithms. Unsafe vs safe Rust is a bit like Ada vs. Spark ("safe Ada"). 'I'd be quite happy to find more people diving into Frama-C': Frama-C is trending upward and Ada is in decline, ever since the Ariane 5 explosion on 4 June 1996. The US DOD consequently shut down its Ada office and eliminated the Ada requirement, and C/C++ subsets increasingly dominated.

philwise 5y ago

Are there vendors who provide support for tool qualification for frama-c? By that I mean documentation support that can be provided as part of the certification process, so when you say "Frama-c verified this code does not contain any arithmetic overflow", it is possible to back that up with "And Frama-c version x.y.z has sound analysis, evidenced by ...."

dandotway 5y ago
Great question. C/C++ is definitely trending upward in 'safe software' systems even though it isn't ready and industry as a whole isn't (as far as I know) using Frama-C. Are Tesla/Google/Apple hiring Ada engineers to build the car autopilots that control whether we live or die? Nope, seems to all be C++, God help us all.