[SystemSafety] C for OSs

[Roderick Chapman]

On 08/09/2019 18:23, Olwen Morgan wrote:
> Rod Chapman and I have a long-standing (and exceedingly civilised :-) 
> difference of opinion in this area. If you have the right tools, and 
> if you are prepared to observe draconian coding discipline, then I 
> believe that you can in C approach a SPARK Ada level of code quality. 
> Rod, if I am not traducing him, has lingering doubts about this. IMO 
> tools are no longer the problem since those who write them simply 
> retrofit sensible formal semantics to (annotation-extended subsets of) 
> C and then perform verifications accordingly.

I still have reservations. The big challenge is to come up with a formal 
semantics that is implemented by both your favourite verification tool 
and all versions of all compilers that you might have to use during the 
lifetime of a project. If you can "lock in" to exactly ONE compiler, 
then things are significantly simpler... but this is not a good place to 
be when, in twenty years time, you really do have to change compiler for 
a hardware update or some other reason, but the vendor has long since 
gone out of business. I see far too many projects stuck in this 
particular rut.

In SPARK, it works by the complete removal of undefined behaviours and 
any dependence on unspecified behaviour. This requires subsetting and 
forms of analysis, which you need to be demonstrably sound and efficient 
enough to scale up to large programs.

I am currently engaged in writing some highly critical C code, using the 
latest Frama-C toolset. I find the experience rather frustrating... the 
problem seems to be two-fold:

1. C is lacking some fundamental features that make SPARK work. (The 
short version: user-defined scalar types, named type equivalence, a 
first-class Boolean type, packages, formal parameter modes, and 
first-class array types).

2. Some very basic things in C are undefined. Worst-offender: signed 
integer overflow.

The upshot is that I find it's very hard to get to an acceptable 
false-positive rate from the Frama-C WP tool. On a recent SPARK project, 
the "acceptable" false alarm rate for type-safety proof was ZERO.. so 
perhaps my expectations are set too high?

Example: in SPARK, we use user-defined scalar types all over the place 
to describe invariants from the problem domain which apply to every 
parameter, constant and variable of each type. That info is used by the 
VC generator to constrain the values of variables, so that proving 
non-overflow becomes tractable. I don't know how to do that in C... (if 
anyone does know how, please help me out...)

  - Rod