Making the world a safer place: self-verifying SMC

We all use code-generators, no matter if we love or hate them (or do both). But for most compilers you simply have to trust that they work correctly and do what they’re supposed to do. They typically do not provide any sort of proof for their correctness. Well, the SMC is different in that regard. It can generate verification code for its C backend.
The idea of self-verifying compilers it not completely new. Several methods have been proposed for this task, proof-carying code and credible compiler to name a few. What I’m doing here is some mixture of both (with a bit more of the credible compiler – altough the SMC is no optimizing compiler, so there is only a single transformation involved). Basically once we generated C code out of the FSM description, we have two (possibly different) FSMs. The one we described and the one SMC generated. The intuitive perception of those two FSMs being equal, is that their languages (dented by \mathcal{L}(F)) are equal. But how do we show that?
For our purpose it’s enough to show that the two transition functions are equal, as we only care about the generated FSM behaving exactly as the described one does. That still leaves us with the problem that we have to unobtrusively check the generated FSM.
Let us define p=(t_1, \dots, t_n), t_i = ((s, \sigma), (s', A_{in}, A_{out}))\in\delta to be a sequence of transitions (called path or trace). We’ll call a path loop free if \forall t: \neg\exists t': t = t' \vee s_t \neq s_{t'} holds – meaning that there are no two transitions within a path having the same start state.
Finally we accept the two FSMs to be equal iff for all loop-free paths in the original FSM, there exists an equivalent path in the generated machine. Following we accept the SMC to work correctly if the two FSMs (orignal one and generated one) are equal.
Generating the traces of the original FSM is a rather trivial task. We already have a good structure to work on (the SMC AST). That’s not the case with the generated FSM. First of all generating the trace must be unobtrusive. We must be sure that our instrumentation does alter the behavior of the FSM. We can accept that a statement of the form


generally does not alter the behavior, if placed appropriate. So we simply place print statements (with a unique ID) at each transition and action. Then we generate code that causes the FSM to transit along the previously determined paths.
If everything goes right, executing that code should cause a sequence of IDs to be printed. In case the SMC works correctly that sequence should be identical to those produced by traces of the original FSM.

To use this verification mechanism, run the SMC with the cverify backend and execute the generated _checker.sh script. That script either ends with “NO ERRORS FOUND” (which should always be the case), with a list of traces which the generated FSM did not perform. Additionally a checker.log file is generated which contains entries like this:

[ ] AST_Transition(_INIT,RT,List(AST_ConstEqCondition(CMD__MODE__RT)),AST_Actions(Some(List(clr)),None)) AST_Transition(RT,_ERR,List(AST_NegatedCondition(AST_PredicateCondition(command))),AST_Actions(None,None))
[!] A98601 T-93118478 T-1152986909 ;
[?] A98601 T-93118478 T-1152986909 ;

where the line marked by the exclamation mark denote the trace of the original FSM, as opposed to question mark which marks trace of the generated FSM.

Ahh, and there is yet another new feature, the SMC can now generate a NuSMV model. Of course that’s all in the repository.

Leave a Reply

Fork me on GitHub