Programming Hotmoka
A tutorial on Hotmoka and smart contracts in Takamaka

Chapter 9 Code verification

Code verification checks that code complies with some constraints, that should guarantee that its execution does not run into errors. Modern programming languages apply more or less extensive code verification, since this helps programmers write reliable code. This can both occur at run time and at compile time. Run-time (dynamic) code verification is typically stronger, since it can exploit exact information about the actual run-time values flowing through the code. However, compile-time (static) code verification has the advantage that it runs only once, at compilation time or at jar installation time, and can prove, once and for all, that some errors will never occur, regardless of the execution path that will be followed at run time.

Hotmoka nodes apply a combination of static and dynamic verification to the Takamaka code that is installed inside their store. Static verification runs only once, when a node installs a jar in its store, or when classes are loaded for the first time at run time. Dynamic verification runs every time some piece of code gets executed.

9.1 JVM bytecode verification

Takamaka code is written in Java, compiled into Java bytecode, instrumented and run inside the Java Virtual Machine (JVM). Hence, all code verifications executed by the JVM apply to Takamaka code as well. In particular, the JVM verifies some structural and dynamic constraints of class files, including their type correctness. Moreover, the JVM executes run-time checks as well: for instance, class casts are checked at run time, as well as pointer dereferences and array stores. Violations result in exceptions. For a thorough discussion, we refer the interested reader to the official documentation about Java bytecode class verification (see https://docs.oracle.com/javase/specs/jvms/se25/html/jvms-4.html#jvms-4.9).