The significance of Model Checking in Tau
In the first step, a program verification problem is reduced to a problem of recursion
scheme model checking. In the second step, the problem of recursion scheme model
checking is solved by reduction to a type checking problem. Thus, our verification
method can be considered an integration of two main previous approaches to program
verification: model checking and type systems.
Model Checking Higher-Order Programs is the title of a paper released relatively recently by Naoki Kobayashi Tohoku University. This particular paper may have influence a design decision in Tauchain which in particular was a switch from Martin Lof Type Theory to Monadic Second Order Logic. In the paper it was discovered that you can do program verification (a method of formal verification) by reducing the problem into a model checking problem for recursion schemes. A program is transformed into a recursion scheme which generates a tree representing all the interesting possible event sequences of the program. In essence the paper reveals the possibility of a recursion scheme model checker.
Trees are interesting indeed
Type-based program analysis. Type systems have been a popular technique for
program analysis and verification [Palsberg 2001]. Various type systems for the resource
usage verification problem considered in Section 3.1 or its variants have been
proposed [Igarashi and Kobayashi 2005; Foster et al. 2002; DeLine and F¨ahndrich
2001; Iwama et al. 2006]. Unlike our method based on higher-order model checking,
those type systems are not complete, and some of them [DeLine and F¨ahndrich
2001] require type annotations.
Connections between types and tree automata have been studied in the context of
languages for XML processing [Hosoya et al. 2005; Benzaken et al. 2003]. They deal
with finite trees, while our type system deals with infinite trees. Type annotations
for recursive functions are required in their languages.
Trees have very interesting behavior and MSOL is particularly interesting over trees. MSOL is Monadic Second Order Logic which has greater expressivity over First Order Logic or Zeroth Order Logic such as predictable or propositional logic. Type theory is an extension of Second Order Logic just as Second Order Logic is an extension to First Order Logic in that it improves expressivity. Martin Lof Type Theory relies on dependent types which produces decidability through type checking.
Conclusion
The approach by Naoki Kobayashi is somewhat new and promising. To have these abilities in Tau would greatly increase the security of the code which runs on Tauchain while possibly reducing the burden on the programmer. Because this is a new approach and the papers are relatively recent there is a lot about the capabilities that remain unknown both for Tauchain and for this approach. The developer of Tauchain Ohad Asor promises to release a whitepaper in the near future to finalize his design decisions and to reveal the initial roadmap which will likely be influenced by or based on the work of Kobayashi.
For security protocols, in any finite state system you can apply a model checker to verify the correctness properties.
References