Contract Verification on a Deterministic JVM (DJVM)

Hi all,

Why do we need a deterministic sandbox?

It is important that all nodes that process a transaction always agree on whether it is valid or not. Because transaction types in Corda are defined using JVM byte code, this means that the execution of that byte code must be fully deterministic. Out of the box, a standard JVM is not fully deterministic, thus we must make some modifications in order to satisfy our requirements.

So, what does it mean for a piece of code to be fully deterministic? Ultimately, it means that the code, when viewed as a function, is pure. In other words, given the same set of inputs, it will always produce the same set of outputs without inflicting any side-effects that might later affect the computation.

What’s the current state of affairs?

In our pursuit of enabling deterministic contract verification in Corda, we have worked on a deterministic sandbox (DJVM) which will provide a safe environment for such verification methods to run in. As part of that work, I have just pushed a pull request for the first iteration of our DJVM work to our Corda repository; see corda/corda#3386. This will form the foundation for the future deterministic sandbox used in Corda. Before we get there though, the code needs thorough review, some further improvements and modifications, etc.

As you will see from the PR, the code in the top-level DJVM module has not yet been integrated with the rest of the platform. It will eventually become a part of the node and enforce deterministic and secure execution of smart contract code, which is mobile and may propagate around the network without human intervention. However, for now it stands alone as an evaluation version.

Preview and request for comments

We want to give developers the ability to start trying it out and get used to developing deterministic code under the set of constraints that we envision will be placed on contract code in the future. For details around the concept, implementation, constraints, scope, etc., please refer to the documentation site. A snapshot of the added documentation can be found on the PR: docs/source/key-concepts-djvm.rst.

NOTE: This is quite a meaty piece of work, and the PR is indeed quite large. I expect there to be quite a few comments and rounds of feedback, and for the PR to be up for a while before merging… and this is indeed the reason for my email – it would be great to get this in front of as many of our users as possible (i.e., you!), for us to perform a thorough review of the work covered by this PR, but also to start thinking about the follow-up work beyond this initial version of the sandbox. This is why I’m calling on anyone interested to take a look and provide feedback.

It should be mentioned that this work ties in closely with our development efforts on the SGX team, working towards a deterministic sandbox for running contract verification inside an SGX enclave. If you’re curious to learn more about that work, have a look at the following material:

• Mike Hearn’s presentation about SGX and Corda (video, blog post)
• Andras Slemmer’s post on our SGX infrastructure design (post)
• Note also that there will be another SGX blog post coming soon (so stay tuned)!

Have a great weekend! Look forward to hearing your feedback on this.

Best regards,

Tommy Lillehagen

Further to my previous email, it’s also worth noting the great work that Chris Rankin has been doing on making deterministic versions of our core and serialisation modules. Here’s a couple of links for reference:

• Create deterministic Core and Serialisation artefacts (corda#3262)
• Deterministic Corda modules (docs site)

Make sure you check those out as well if you’re interested in this topic.

Thanks Tommy – this is great!  There seems to be interest beyond the Corda community judging by the number of retweets and comments I received over the weekend when I publicised your first post.  I’ll share it some more during working hours too.  I think it’s really important that we get the eyes of the broader Java community on this ☺

Richard

richard@... . www.r3.com

I've posted two Medium stories on the topic:

·         Deterministic Contract Verification

·         DJVM Behind the Scenes