ISoLA 2018: Thoughts on X-by-Construction

Expressing what you want

The first point in ensuring any particular property, whether by construction or not, is to be able to specify this property. This is harder than it might seem!

The Extremes

So let’s start with the extremes: assume we have a language for modelling state machines. One particular — and very trivial — aspect of correctness might be that every state machine has at most one start state. The IDE has the usual graphical editor with a palette. Let’s say that the IDE prevents you from dropping a start state symbol onto your canvas if there is already one. So you physically cannot create a model that violates this (admittedly trivial) correctness constraint. This is clearly correctness by construction.

Between the Extremes

Let’s say the state machine language lets you drop a second start state onto the canvas, but then immediately marks it as an error with a red squiggly. Or for a more advanced property which we can specify using temporal logic, every change to the machine (or property) triggers a model check that comes back with an error (or not) after a reasonable time, so the feedback happens “during construction”. Strictly speaking, you were able to construct a faulty model, but you were made aware of the error immediately. Does this count as “by construction”? If you say yes, then basically every interactive program analysis such as type systems is part of correctness-by-construction. That’s fine, but the “by construction” starts to lose its meaning a bit.

Transformations

Often the scenario is slightly more complicated because a transformation step is involved. Say your state machine is correct as defined on the level of the model (take the “only one start state” as an example or a valid model check of your temporal properties with NuSMV). Now you translate it. How do you know that the result of the transformation is correct?

DSLs without by-construction?

This hints at an interesting middle ground: use a nice DSL to specify your model and then exploit the domain semantics for generating code that implements the semantics together with properties that check those semantics on the code level. And yes, ideally you should prove those correct, but maybe you can make do with a slightly weaker guarantee: make sure the implementation generator and the property generator are developed independently to avoid common-cause errors. It is then very unlikely that the implementation and the properties are “compatibly broken”. Not sure it qualifies as correct-by-construction, though. This is basically what we did in the Voluntis project.

Correctness vs. Security

If we look at security-by-construction, then things become even harder. A slightly colloquial way of distinguishing security from correctness is that correctness specifies what exactly the system should do. And security ensures that it does not do anything else (which could then presumably be exploited). Staying with our state machine, one that is secure with respect to this definition is one that is fully specified, i.e., we define the reaction to every event in every state. There are no “unspecified behaviors” left to be exploited.

Loose Ends

Here are two few more things to think about. A development process that puts X first, and ensures, through process and methodology that X holds in the developed system is not X-by-construction. You can maybe call it X-by-design, and it is certainly useful, but it is different.

Wrap-Up

I think we have two options. We either have to widen the definition of X-by-Construction to the point where it includes pretty much everything that mechanically finds violations of X before we deploy/ship/run the system. But then it’s a distinction without a difference. Or we stay with the strict definition, but then we require proofs, either of the transformation of the program or of the transformation of the properties. For realistic system sizes in realistic (industry) contexts I think we are quite a ways away from this.

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Markus Voelter

Markus Voelter

software (language) engineer, science & engineering podcaster, cross-country glider pilot. On medium mostly for the software stuff.