4 ms·

C program proofs with Frama-C and its weakest-precondition plugin [pdf]

fizixer 6y ago
So this system uses the spec language ACSL (I assume it's a formal spec language, FSL). How widely used is it? I've heard of TLA+ being very popular. Then there is Z notation, and about half a dozen or more others. If there is no standard FSL, do I have to learn a new FSL everytime I want to apply formal methods to a slightly different system I'm working with? Formal methods is a hard enough area. Lack of standardization makes it harder.
- Firobe 6y ago
  ACSL is indeed a FSL. Making a standard FSL is a nigh impossible since it should encompass every programming language and its specific features. For example, ACSL has built-in ways to talk about the side effects in C, labels, the validity of pointers, etc. and the semantic of those elements is tied to the C standard. On the other hand, the syntax of ACSL is heavily inspired from JML (FSL for Java) which is pretty popular. So if you know JML, it's easy to learn ACSL (you just have to learn C-specific features)
ngneer 6y ago
I remember Frama-C for its slicing. I have recently become interested in Datalog driven approaches, such as Souffle, for static analysis of large codebases. Anyone with experience or thoughts along those lines?
- e79 6y ago
  Out of curiosity, are there known pros and cons to each approach? I’ve been experimenting with Z3’s CHC engine and Coq for modeling programs. I don’t know enough about both yet to fully understand how they compare.
therein 6y ago
I wasn't sure what WP stood for. My mind jumped to WordPress but that obviously wouldn't make sense. Turns out it stands for Weakest Precondition.
- dang 6y ago
  Hmm, good point. We've put weak preconditions in the title above.
Animats 6y ago
Interesting. Using a fully automatic SAT solver for the easy stuff and Coq for the things the SAT solver can't prove maker good sense. We did that 40 years ago in the Pascal-F system. The Oppen-Nelson cooperative decision procedure system (the first SAT prover) did the easy stuff - proofs that only need addition, subtraction, multiplication by constants, and logic. Beyond that you had to write a "rule" and prove it with the Boyer-Moore prover, which is a constructive system that uses induction. About 95% of the verification conditions were solved without adding new rules. This group got about as far as we did - arrays, but not dynamic allocation, pointers, or objects. "WP cannot currently work with dynamic allocation, " they write. That's the point at which describing what "valid" means becomes difficult, and you get into specification languages separate from the program. I notice they put in what they called "ghost code", code which has meaning only at proof time. We called that "proof code". It's written in the same language as the real code, and can look at values from the output, but can't change them. This is a programmer-friendly way to write specifications. It's easy to write code to check a sort or a lookup if you're not concerned about speed or space. Then you prove that the dumb check and the complex algorithm get the same result. One big problem with proof of correctness systems is that they tend to be designed by people in love with the formalism. They need to be designed by people who hate and fear bugs. The Microsoft Static Driver Verifier is probably the best example of a system aimed squarely at preventing crash-type bugs. It's the main tool Microsoft used to prevent drivers from crashing Windows 7 and later.
- docandrew 6y ago
  I've read very little detail about the Static Driver Verifier other than that it's supposed to use an SMT solver. I don't know if MS is using the same tool for other products in their portfolio or not. I've used it a little bit (it's a pain to set up) but have little information about exactly what it does, since it doesn't rely on any special annotations or specification language. Can you shed any light on more technical details about it? With F*, Dafny and the Lean theorem prover, it seems like Microsoft (at least the research division) is moving in the direction of formal verification but I hear very little about it's use on their commercial products. Trade secret, perhaps?
  - 6y ago

So this system uses the spec language ACSL (I assume it's a formal spec language, FSL). How widely used is it? I've heard of TLA+ being very popular. Then there is Z notation, and about half a dozen or more others. If there is no standard FSL, do I have to learn a new FSL everytime I want to apply formal methods to a slightly different system I'm working with? Formal methods is a hard enough area. Lack of standardization makes it harder.

Firobe 6y ago
ACSL is indeed a FSL. Making a standard FSL is a nigh impossible since it should encompass every programming language and its specific features. For example, ACSL has built-in ways to talk about the side effects in C, labels, the validity of pointers, etc. and the semantic of those elements is tied to the C standard. On the other hand, the syntax of ACSL is heavily inspired from JML (FSL for Java) which is pretty popular. So if you know JML, it's easy to learn ACSL (you just have to learn C-specific features)

ngneer 6y ago

I remember Frama-C for its slicing. I have recently become interested in Datalog driven approaches, such as Souffle, for static analysis of large codebases. Anyone with experience or thoughts along those lines?

e79 6y ago
Out of curiosity, are there known pros and cons to each approach? I’ve been experimenting with Z3’s CHC engine and Coq for modeling programs. I don’t know enough about both yet to fully understand how they compare.

therein 6y ago

I wasn't sure what WP stood for. My mind jumped to WordPress but that obviously wouldn't make sense. Turns out it stands for Weakest Precondition.

dang 6y ago
Hmm, good point. We've put weak preconditions in the title above.

Animats 6y ago

Interesting. Using a fully automatic SAT solver for the easy stuff and Coq for the things the SAT solver can't prove maker good sense. We did that 40 years ago in the Pascal-F system. The Oppen-Nelson cooperative decision procedure system (the first SAT prover) did the easy stuff - proofs that only need addition, subtraction, multiplication by constants, and logic. Beyond that you had to write a "rule" and prove it with the Boyer-Moore prover, which is a constructive system that uses induction. About 95% of the verification conditions were solved without adding new rules. This group got about as far as we did - arrays, but not dynamic allocation, pointers, or objects. "WP cannot currently work with dynamic allocation, " they write. That's the point at which describing what "valid" means becomes difficult, and you get into specification languages separate from the program. I notice they put in what they called "ghost code", code which has meaning only at proof time. We called that "proof code". It's written in the same language as the real code, and can look at values from the output, but can't change them. This is a programmer-friendly way to write specifications. It's easy to write code to check a sort or a lookup if you're not concerned about speed or space. Then you prove that the dumb check and the complex algorithm get the same result. One big problem with proof of correctness systems is that they tend to be designed by people in love with the formalism. They need to be designed by people who hate and fear bugs. The Microsoft Static Driver Verifier is probably the best example of a system aimed squarely at preventing crash-type bugs. It's the main tool Microsoft used to prevent drivers from crashing Windows 7 and later.

docandrew 6y ago
I've read very little detail about the Static Driver Verifier other than that it's supposed to use an SMT solver. I don't know if MS is using the same tool for other products in their portfolio or not. I've used it a little bit (it's a pain to set up) but have little information about exactly what it does, since it doesn't rely on any special annotations or specification language. Can you shed any light on more technical details about it? With F*, Dafny and the Lean theorem prover, it seems like Microsoft (at least the research division) is moving in the direction of formal verification but I hear very little about it's use on their commercial products. Trade secret, perhaps?
- 6y ago