>> Welcome to our talk about
model-based testing with TLA+ and Apalache.
This is a joint work of Igor Konnov and myself.
We both are proud to be members of Informal Systems.
Igor Konnov is the Principal Scientist
developing next generation verification methods.
He's also the Leading Developer of Apalache model checker.
I'm a Research Engineer at Informal who also contributes to
Apalache and leads the product on model-based testing.
[MUSIC]
>> We're using Rust Informal verification tools to
build open source fault-tolerant distributed systems,
like the Tenement Byzantine Fault Tolerant Consensus engine
and the Inter-Blockchain Communication protocol.
We're cooperatively owned and governed by our employees.
We have offices in Toronto,
Berlin, Vienna, and Lausanne.
In fact, a few of the folks at Informal would love to say hello.
>> Hello.
>> Hello, world.
>> Hi.
>> Hi, everyone.
>> Hello.
>> Hey, everyone.
>> Hello.
>> Hi.
>> Hey, everyone.
>> You can learn more about us, check out our work,
and contribute online at github.com/informalsystems.
We hope you enjoy the conference.
[MUSIC]
>> Who we are. At Informal Systems,
we envision the bright future
of verifiable distributed systems and organizations.
Nowadays, everything becomes distributed.
At the same time, when we interact with systems and organizations,
we need a certain level of trust.
Our grand vision is that formal verification can help us to bring
this necessary level of trust to
the systems and organizations with whom we interact.
We actively contribute to this future vision by
developing the next-generation blockchain infrastructure,
named as a Tendermint blockchain consensus protocol
and the Inter-Blockchain Communication protocols.
Our formal verification portfolio
consists of the Apalache model checker,
one of the leading model checkers for TLA+.
We also contribute to
this verifiable organization's vision with Themis Contract.
Our infrastructure power is the Cosmos network.
The Cosmos network is a dream vision of
the next generation Internet of blockchains,
where each blockchain can operate independently.
At the same time, these blockchains
can interact and trust each other.
How do we choose this trust?
We propose verification-driven development framework.
We have applied this framework to our own products,
namely, to the Tendermint family of protocols.
We have developed English
and TLA+ specifications of these protocols,
model checks, and with Apalache.
This has helped us to fix
some protocol issues, but, most importantly,
it helped to clarify
the mutual protocol understanding
between the research and the development teams.
What's not so nice about this is that we have realized that,
after we start to develop code,
the code starts to diverge from the specifications.
You see that the necessary feedback loop is missing here.
The way we propose to address
this issue is by model-based testing.
In model-based testing, we generate
integration tests from simple TLA+ assertions.
This helps us to eliminate
the divergence between the spec and the code,
they now evolve in sync.
This significantly improves ease of writing and using the tests.
Also, it improves the test maintainability and
helps us to achieve higher code coverage.
This is a teaser of our model-based testing process.
But before diving into it,
Igor will tell you more about the Tendermint protocols,
the Light Client protocol,
and the Apalache model.
>> Hey, my name is Igor Konnov.
I'm a Principal Researcher at Informal Systems.
I will give you a brief introduction into Tendermint light client,
how we specify it in TLA+,
and I'll give you an interaction in
the model checking results with Apalache.
Then Andrey Kuprianov will continue to
talk with model-based testing.
Let's have a look at Tendermint blockchain. What is that?
That's a sequence of blocks,
and every block has a certain structure.
There are interesting fields here,
one of them is a validator set.
This is set of computers that are going to vote on this block.
When more than two-thirds of them vote on the block,
this block is going to be added on the blockchain.
There is an algorithm which is called Tendermint Consensus,
and all of these validators are running this algorithm.
What these validators are deciding on,
they decide on the contents of this block,
the application state in this block.
They also decide on who the next validators are going to be.
When they have decided that, the validators change.
The set of validators might change.
When this block has been committed,
there is another record that is formed in the next block,
which is called LastCommit.
This record contains the votes
of the validators from the previous block,
and the cache that this points into previous block.
If you're running Tendermint Consensus as a validator,
you can make sure that your
transactions that you have submitted on the blockchain,
you can figure out whether they have been committed or not.
But what happens if you just have a smartphone?
You cannot run Tendermint Consensus on it.
It's just too expensive and you don't want to
invest a lot of money into running the validator.
That is the question, how the light client is solving.
The light client who have some trust in block, say Block 1.
It doesn't matter how you figured out whether to trust it or not,
but you know you can trust it.
Then you want to download
another block that is far on the blockchain.
You cannot trust anyone.
You cannot trust the peers that give you the blocks.
You have to use some knowledge about these blockchain
to figure out whether you can trust the block. What can you do?
Say, if you want to download Block 9,
the obvious solution would be to download the whole blockchain,
check all these digital signatures,
check how many validators have
voted for each block, and so on and so forth.
But that's too expensive, especially
if you do it on a mobile phone.
Fortunately, we can do what is called skipping verification.
It's using the knowledge about how this consensus is working.
First of all, there is one interesting observation here.
If I know that my block was committed by a set of validators,
and more than one-third of
these validators using the validators in a trusted block,
then I know that at least one of
the validators can be trusted because they
have less than one series of false validators in our system.
That's basically the idea.
If you find a pair of blocks,
such that you can establish this root of trust,
you can trust the new block.
Then do bisection again and find
these pairs of blocks that can establish the trust.
Basically, skipping verifications doing some formal bisection.
There is one complication though.
First of all, I have to make sure that
more than one validators has voted.
Second, I have to know something about time because,
in Tendermint, you don't put your money at stake forever.
You put it for some time.
It's just called unbonding period.
If I'm running the validator for, say, Block 1,
it means that I have staked some money,
and this money is going to be lost if
I do something wrong on the blockchain.
That's why it's not sufficient just
to check how many validators have voted,
you also have to figure out that
all these validators are still using
what is called the trusting period.
You have to find that more than one-third of validators has voted,
and your time is in
the trusting period of those validators
who have voted on the trusted block.
As we have seen, Tendermint Consensus,
the assumptions about the blockchain,
and the Light Client protocol, they are not simple.
That's why we have decided to formalize these assumptions
in TLA+ and check them with a model checker.
But before we actually sat down and wrote a TLA+ specification,
we wrote another document,
in which we called English Specification.
That's how we do things at Informal Systems now.
We write this document,
it's a mixture of English prose and Mathematics campaigns,
the sequential statement about
the problem they are going to solve.
It's a composition of this problem into distributed components.
It also has basic specifications
on the temporal purposes we believe this protocol should satisfy.
It has the high level functions,
the pre-conditions, the post-conditions, and more importantly,
the error conditions that tell us what has
to happen if some assumptions about our system are violated.
The user's document has a base
for discussions between [inaudible] with the system engineers,
verification engineers, and researchers before
we start diving into a formal specification,
such as one in TLA+.
I am not going to give you this document here,
but you can find it on the web. Here's a link.
You can see how one
can understand this Light Client protocol without TLA+.
Once this document is ready,
we sit down and write a specification in TLA+.
In case of Light Client,
it actually took us several hours to translate
the English specification into
actual TLA+ that we could check with Apalache.
What we focus on in the TLA+ specification,
we focus on the model of
the blockchain that I briefly explained to you before.
This model captures these notions of validator sets,
Byzantine faults, and the time assumptions
that we have in Tendermint Consensus.
We have a specification of the Light Client protocol in TLA+.
In our case, the Light Client protocol is talking to a peer.
Here is correct, or faulty,
and it also has some time that it relates to the blockchain.
Again, I'm not giving you the TLA specification,
you can find that on the web.
But I want to give you a bit of flavor about this specification.
First of all, the light client can talk
to either a faulty peer or a correct peer.
The light client, of course, cannot
know whether the peer is faulty or not,
but it will set up
a parameter in the specification it is telling us,
whether the peer is faulty or not.
If the peer is correct,
we just copy a block from
the blockchain and give it to the light client.
If the peer is faulty,
we produce a non-premise block
that passes some basic validation tests,
but it might have the incorrect set of validators,
or it may have an incorrect set of commits,
it might have some skewed time and so on and so forth.
I just want to show you here the structure
of the blocks that you have because it might be interesting.
Blocks are basically records sincerely,
they have the height, the time,
which is just an integer now in coding.
They have a set of commits.
These are the validators who have voted on the previous block,
they have this set of validators for the current block,
and they have this set of validators for the next block.
When a client is receiving a LightBlock,
it gets this header plus this set of commits,
who must have voted on that header.
If you think about checking these data structures,
you'll see a margin, you have a sequence of logs there.
You can see that there is a lot of space for state explosion.
Here you have integer time and you have four sets of validators.
That's why they are usually Apalache.
Again, I'm not giving you details,
I have all details here.
But basically, before you get on the light client,
we initialize the blockchain just in one step,
and when we initialize it we just guess the validator sets,
the sets of commits and time stamps,
so they form a correct blockchain
where more than two-thirds of validators have voted,
also correct and not correct timestamps
are grown on a time period.
Let's see how we can verify
the specification on the light client with our model checker.
Apalache, if you haven't seen this tool before,
you can go on that webpage that's mention above.
Read the manual and see for yourself how it's working.
From the bird's eye perspective,
what it does, it takes the TLA specification,
it unfolds all the operator definitions,
including the recursive operator definitions up to
certain bounds and finds what we call assignments.
Similar to what you'll see this dynamically.
It decomposes a specification into
smaller pieces that we call symbolic transitions,
roughly corresponds to actions and the specification,
then it does some simple tab checking.
Although what it does now is going to be
superseded by the new type checker
and type inference you heard about.
This means magnet as well.
Then it does a translational,
particularly specification into SMT solver.
As you probably know, SMT solver is quite powerful and we want to
utilize their power for verification questions in TLA+.
What Apalache does in a bit more detail,
it actually performs bounded model checking.
Given a specification in the following canonical form that tells,
you also expect Apalache
first checks whether the environment can be evaluated.
The initial state translates this formula into SMT and
pass this SMT solver if it can
find a satisfying assignment for this query.
If it has found a satisfying assignment,
Apalache will produce a counterexample in TLA form.
Otherwise, it will continue to unroll executions,
it'll introduce one step, two steps,
three steps, until it has either found a counterexample with
SMT or it has reached a certain depth.
That's why it's called Bound Model Checking.
Fortunately, for the light client's specification,
you can provide the depths given the length of the blockchain.
Re-run Apalache on different models
produced from the light client specification.
There we had from 4-7 validators and
from 3-5 blocks in the blockchain.
Also, we had either faulty or correct peers,
the light client was talking to.
This set of huge numbers, however,
recalls that we had all this power sets in
the blockchains and
three key relations including cardinality comparisons.
We also have found some violations of the purposes,
which is interesting because these violations were
predicted by our researchers.
I just want to show you how Apalache runs.
Without any compilation or whatever,
you can just pull the tool from Docker,
it will pull a Docker image.
In my case, it's fresh,
so it doesn't do anything.
Then they run the Docker image around Apalache.
The Docker image asks you to check this variant and
give it the model of five validators and five blocks.
What Apalache does now inside the Docker image,
it does the pre-processing I told you about.
Then it checks the invariant for the initial state,
all possible states after one step, after two steps,
after three steps, and soon it's going to report a counterexample.
Here's a counter-example.
We can go to counter-example of a TLA and
see the exact values produced by Apalache,
and you see that violates these specific invariants.
Now, I give the floor to Andrey.
>> Now, we continue with the model-based testing.
But before diving into it,
I want to describe how standard testing looks as before.
A test engineer who uses a tendermint-go
implementation to manually write
integration tests that goes round
against both tendermint-rs and tendermint-go implementations.
This is an example of
a pretty simple manually written integration test.
It just constructs a test case,
which is a sequence of steps for the light plan protocol.
Then this test case is translated into the JSON and
all the necessary data structures which contain
such details as public keys and hashes.
It's executed by the static driver
and this static driver is a pretty simple piece
of code which just takes this case,
executes the light plan verifier and
compares it to returns at each step,
the deep sets expected from the test.
Standard testing has a number of drawbacks.
First of all, it's manual generation.
With lots of effort,
this test that we solved was pretty simple, actually.
More complicated cases, it's non-trivial logic
required and it's inflexible.
It fixes all the parameters,
non determinism left or exploration.
It's also hard to understand what the particular test case does.
Its hard to maintain them and it's hard to cover
all the case because we will need hundreds of those tests.
Next, I will switch to model-based testing.
Now, we will look at its components.
But before looking at that particular view,
we will run a short demo.
This is a short demo of how our model-based testing is working.
It's fully integrated into
the standard cargo test command as a test.
But when we run this cargo test,
among what happens for each of the TLA+ tests,
in this case it's a success,
it runs Apalache on this test.
Apalache produces a counterexample
which contains the example execution.
This execution is then translated into the static test,
and this test is run against the implementation.
In this case, we have the light client protocol and we execute
this light client protocol against the static test and compare
the verdict that we obtain against the expected verdict.
What we can see in this case is that
running Apalache does take some time.
But as a byproduct of those model-based test,
we obtain a static tests,
and this static test can then be executed
independently in almost no time.
Now, how does a TLA+ test look like?
TLA+ test is a pretty simple TLA+ resource.
It's very easy to understand for
each particular test what it does.
I very much like, for example.
This test says that for each state in the computational history,
the validator sets would be different.
You can also express assertions about time,
for example, or about the final state of the protocol.
How do we integrate this test
with the LightClient model you saw before?
This is also very easy due to
the modular nature of the TLA+ language.
We simply extend the Init and Next predicates,
we use the history tracking.
I've introduced this additional history variable,
and this variable just tracks
the necessary state components of the LightClient protocol,
and at each step of
the model execution besides executing this model itself,
we're also updating the history for the next step.
For the model checker, we needed only to extend it to
this JSON input-output support for integration purposes.
In fact, you can now use Apalache
as a translator between TLA+ and JSON,
and we highly encourage everyone interested to use this feature.
You could use it, for example,
to integrate TLA+ with your tools.
Now, how counterexample looks like,
a counterexample is a sequence of history states.
At each state of this history we have the current block,
the current time point,
the verdict that we expect from the LightClient,
and the latest verified block.
This has covered a small portion of
this history it translated into JSON.
Don't be discouraged by the large size of the encoding,
this is meant only for automatic purchase.
Now, as a next step we transform
our counterexample with the help of
another component which is called
JSONata into the static integration test.
This transformation happens with
the help of so-called transformation specification,
which is a small domain-specific language.
We described how to transform one JSON into another JSON.
An important part of this translation is that it calls
so-called tendermint-testgen command which allows us to
produce whole Tender mint data structures
from the abstract data structures that we have in the TLA+ model.
Let's take a look at how TestGen works.
Effectively, you can see it as a prob into
the concrete implementations space from the abstract TLA+ space.
For example, in the abstract space it will
identify as a simple string identifier.
In the concrete implementation space,
it contains private and public keys and additional details.
A header in the abstract space just lists
all simple abstract details like the validator sets,
the Next validator sets,
the height, the time, and the lastCommit.
This translates into a fully-fledged data structure
with all the necessary hashes.
Now, to the results. One of
the most important result about model-based testing is,
from my point of view,
that it help to eliminate
the divergence between the spec and the code.
Each case that you see here results
from a fail in model-based test for example,
it was able to gauge
such corner cases as the difference between less,
and less than or equal.
In this particular case,
the TLA+ specification actually diverts both from
the English specification and from the source code.
In another cases, we edit, for example,
additional condition to the specification
because it will generate in
negative times because it was simply integers.
Then another corner case in less than equal and less.
It was also missing another check in the specification,
that the headers are not coming from the future.
Model-based testing helped us to substantially
improve the goal coverage as you can
see for the relevant parts of the source tree,
and it already helped us to find the real bug.
All of this is on the first iteration.
Recently, we have updated
the Tendermint protocol from version 033 to version 034,
and the validators are set ordering change between the version.
An important aspect here is that this bug was missed both by
the standard testing and it was also
not properly documented in the specifications of the product,
but it was caught by the model-based test.
It was a pretty simple fix, as you can see here.
Now, to conclude, model-based testing
substantially improves ease of writing and uses of tests.
It's much easier to maintain
them and it improves the code coverage.
The most important aspect I think is
that it makes the specifications live.
Now, a specification evolves
continuously with the code that it specifies.
Although we have invested some time into infrastructure,
I think the benefits substantially outweigh those investments.
As a future work,
currently we are working on adding fuzzing to model-based testing,
and the fuzzing will understand
additional mutation on the level of data structures.
This allows us to cover scenarios which
are currently inexpressible in the abstract model.
For example, in the abstract model
a validator set is a mathematical set,
so it can't contain two identical validators.
At the same time for the source code,
you want to test such cases.
We plan to add extensions to the Apalache model checker for
faster counterexample search because counterexamples
can be found using specialized techniques.
Currently, Apalache is more attached towards invariant checking.
We plan to generate executable code from TLA+ specifications,
and this means just resolving
the old monitoring mechanisms that is present in the TLA+.
This will allow us to substantially speed up testing.
We plan to extend
the model-based testing framework to
distributed setting where we will cut
the system at the interface points and
replace some of the models with executable specifications,
and that's where we will test
a mixture of the specs and the real code in the running system.
Thank you for your attention.