(image)

Programming Hotmoka
A tutorial on Hotmoka and smart contracts in Takamaka

9.2 Takamaka bytecode verification

Hotmoka nodes verify extra constraints, that are not checked as part of the standard JVM bytecode verification. Such extra constraints are mainly related to the correct use of Takamaka annotations and contracts, and are in part static and in part dynamic. Static constraints are checked when a jar is installed into the store of a node, hence only once for each node of a network. If a static constraint is violated, the transaction that tries to install the jar fails with an exception. Dynamic constraints, instead, are checked every time a piece of code is run. If a dynamic constraint is violated, the transaction that runs the code fails with an exception.

Below, remember that @FromContract is shorthand for @FromContract(Contract.class). Moreover, note that the constraints related to overridden methods follow by Liskov’s principle [13].

Hotmoka nodes verify the following static constraints:

  • 1. The @FromContract(C.class) annotation is only applied to constructors of a (non-strict) subclass of io.takamaka.code.lang.Storage or to instance methods of a (non-strict) subclass of io.takamaka.code.lang.Storage or of an interface.

  • 2. In every use of the @FromContract(C.class) annotation, class C is a subclass of the abstract class io.takamaka.code.lang.Contract.

  • 3. If a method is annotated as @FromContract(C.class) and overrides another method, then the latter is annotated as @FromContract(D.class) as well, and D is a (non-strict) subclass of C.

  • 4. If a method is annotated as @FromContract(D.class) and is overridden by another method, then the latter is annotated as @FromContract(C.class) as well, and D is a (non-strict) subclass of C.

  • 5. If a method is annotated as @Payable, then it is also annotated as @FromContract(C.class) for some C.

  • 6. If a method is annotated as @Payable, then it has a first formal argument (the paid amount) of type int, long or BigInteger.

  • 7. If a method is annotated as @Payable and overrides another method, then the latter is annotated as @Payable as well.

  • 8. If a method is annotated as @Payable and is overridden by another method, then the latter is annotated as @Payable as well.

  • 9. The @Payable annotation is only applied to constructors of a (non-strict) subclass of the library class io.takamaka.code.lang.Contract or to instance methods of a (non-strict) subclass of io.takamaka.code.lang.Contract or of an interface.

  • 10. Classes that extend io.takamaka.code.lang.Storage have instance non-transient fields whose type is primitive (char, byte, short, int, long, float, double or boolean), or is a class that extends io.takamaka.code.lang.Storage, or is any of java.math.BigInteger, java.lang.String, java.lang.Object or is an interface (see Sec. 3.5).

    The choice of allowing, inside a storage type, fields of type java.lang.Object can be surprising. After all, any reference value can be stored in such a field, which requires to verify, at run time, if the field actually contains a storage value or not (see the dynamic check number 5 at the end of this section). The reason for this choice is to allow generic storage types, such as StorageTreeMap, whose values are storage values as long as K and V are replaced with storage types. Since Java implements generics by erasure, the bytecode of such a class ends up having fields of type java.lang.Object. An alternative solution would be to bound K and V from above (StorageTreeMap). This second choice would be erased by using Storage as static type of the erased fields of the class. However, not all storage reference values extend Storage. For instance, this solution would not allow one to write StorageTreeMap, where both String and BigInteger are storage types, but neither extends Storage. The fact that fields of type java.lang.Object or interface actually hold a storage value at the end of a transaction is checked dynamically (see the dynamic checks below).

  • 11. There are no static initializer methods.

    Java runs static initializer methods the first time their defining class is loaded. They are either coded explicitly, inside a static {…} block, or are implicitly generated by the compiler in order to initialize the static fields of the class. The reason for forbidding such static initializers is that, inside Takamaka, they would end up being run many times, at each transaction that uses the class, and reset the static state of a class, since static fields are not kept in blockchain. This is a significant divergence from the expected semantics of Java, that requires static initialization of a class to occur only once during the lifetime of that class. Note that the absence of static initializers still allows a class to have static fields, as long as they are bound to constant primitive or String values.

  • 12. There are no finalizers.

    A finalizer is a method declared exactly as public void finalize() {…}. It might be called when the JVM garbage collects an object from RAM. The reason for forbidding such finalizers is that their execution is not guaranteed (they might never be called) or might occur at a non-deterministic moment, while code in blockchain must be deterministic.

  • 13. Calls to caller() occur only inside @FromContract constructors or methods and always on this.

  • 14. Calls to constructors or methods annotated as @FromContract occur only in constructors or instance methods of an io.takamaka.code.lang.Contract; moreover, if they occur, syntactically, on this, then they occur in a method or constructor that is itself annotated as @FromContract (since the caller() is preserved in that case).

  • 15. Bytecodes jsr, ret and putstatic are not used; inside constructors and instance methods, bytecodes astore 0, istore 0, lstore 0, dstore 0 and fstore 0 are not used.

    Local variable 0 is used to hold the this reference. Forbidding its modification is important to guarantee that this is not reassigned in code, which is impossible in Java but perfectly legal in (unexpected) Java bytecode. The guarantee that this is not reassigned is needed, in turn, for checking properties such as point 13 above.

  • 16. There are no exception handlers that may catch unchecked exceptions (that is, instances of java.lang.RuntimeException or of java.lang.Error).

    By forbidding exception handlers for unchecked exceptions, it follows that unchecked exceptions will always make a transaction fail: all object updates up to the exception will be discarded. In practice, transactions failed because of an unchecked exception leave no trace on the store of the node, but for the gas of the caller being consumed. The reason for forbidding exception handlers for unchecked exceptions is that they could occur in unexpected places and leave a contract in an inconsistent state. Consider for instance the following (illegal) code: 

    try {
    this.list.add(x);
    x.flagAsInList();
    this.counter++;
}
catch (Exception e) { // illegal in Takamaka
}

    • Here, the programmer might expect that the size of this.list is this.counter and the correctness of his code might be based on that invariant. However, if x holds null, then an unchecked NullPointerException is raised just before this.counter could be incremented, and that exception would be caught and ignored. The expected invariant would be lost. The contract will remain in blockchain in an inconsistent state, for ever. The situation would be worse if an OutOfGasException would be caught: the caller might provide exactly the amount of gas needed to reach the flagAsInList() call, and leave the contract in an inconsistent state. Checked exceptions, instead, are explicitly checked by the compiler, which should ring a bell in the head of the programmer.

    For a more dangerous example, consider the following Java bytecode: 

    10: goto 10
exception handler for java.lang.Exception: 10 11 10 // illegal in Takamaka

    This Java bytecode exception handler entails that any OutOfGasException thrown by an instruction from line 10 (included) to line 11 (excluded) redirects control to line 10. Hence, this code will exhaust the gas by looping at line 10. Once all gas is consumed, an OutOfGasException is thrown, that is redirected to line 10. Hence another OutOfGasException will occur, that redirects the executor to line 10 again. And so on, for ever. That is, this code disables the guarantee that Takamaka transactions always terminate, possibly with an OutOfGasException. This code could be used for a DOS attack to a Hotmoka node. Although this code cannot be written in Java, it is well possible to write it directly, with a bytecode editor, and submit it to a Hotmoka node, that will reject it, thanks to point 16.

  • 17. If a method or constructor is annotated as @ThrowsExceptions, then it is public.

  • 18. If a method is annotated as @ThrowsExceptions and overrides another method, then the latter is annotated as @ThrowsExceptions as well.

  • 19. If a method is annotated as @ThrowsExceptions and is overridden by another method, then the latter is annotated as @ThrowsExceptions as well.

  • 20. Classes installed in a node are not in packages java.*, javax.* or io.takamaka.code.*; packages starting with io.takamaka.code.* are however allowed if the node is not initialized yet.

    The goal of the previous constraint is to make it impossible to change the semantics of the Java or Takamaka runtime. For instance, it is not possible to replace class io.takamaka.code.lang.Contract, which could thoroughly revolutionize the execution of the contracts. During the initialization of a node, that occurs once at its start-up, it is however permitted to install the runtime of Takamaka (the io-takamaka-code-1.8.1.jar archive used in the examples in the previous chapters).

  • 21. All referenced classes, constructors, methods and fields must be white-listed. Those from classes installed in the store of the node are always white-listed by default. Other classes loaded from the Java class path must have been explicitly marked as white-listed in the io-hotmoka-whitelisting-1.11.5.jar archive.

    Hence, for instance, both the support classes io.takamaka.code.lang.Storage and io.takamaka.code.lang.Takamaka are white-listed, since they are defined inside io-takamaka-code-1.8.1.jar, that is typically installed in the store of a node during its initialization. Classes from user jars installed in the node are similarly white-listed. Method java.lang.System.currentTimeMillis() is not white-listed, since it is loaded from the Java class path and is not annotated as white-listed in io-takamaka-whitelisting-1.11.5.jar.

  • 22. Bootstrap methods for the invokedynamic bytecode use only standard call-site resolvers, namely, instances of the resolvers java.lang.invoke.LambdaMetafactory.metafactory or java.lang.invoke.StringConcatFactory.makeConcatWithConstants.

    This condition is needed since other call-site resolvers could call any method, depending on their algorithmic implementation, actually side-stepping the white-listing constraints imposed by point 21. Java compilers currently do not generate other call-site resolvers.

  • 23. There are no native methods.

  • 24. There are no synchronized methods, nor synchronized blocks.

    Takamaka code is single-threaded, to enforce its determinism and avoid deadlock. Hence, there is no need to use the synchronized keyword.

  • 25. Field and method names do not start with a special prefix used for instrumentation, namely they do not start with §.

    This condition avoids name clashes after instrumentation. That prefix is not legal in Java, hence this constraint does not interfere with programmers. However, it could be used in (unexpected) Java bytecode, that would be rejected thanks to point 25.

  • 26. Packages are not split across different jars in the classpath.

    This condition makes it impossible to call protected methods outside of subclasses and of the same jar where they are defined. Split packages allow an attacker to define a new jar with the same package name as classes in another jar and call the protected methods of objects of those classes. This is dangerous since such methods often access or modify sensitive fields of the objects.

    • Takamaka verifies the following dynamic constraints: