Skip to content

Commit

Permalink
[Move-prover] Dave's paper edits
Browse files Browse the repository at this point in the history 
I've rewritten and edited various things.

I tried to emphasize the three transformations that improved
performance, and added (what I think are) some catchy names:
alias-free memory model and fine-grained invariant checking.

I've done some word and grammar smithing.

I've suggested some things that can be cut for space because
they're good but not central to our point.

Closes: aptos-labs#9371
  • Loading branch information
@DavidLDill @bors-libra
DavidLDill authored and bors-libra committed Oct 9, 2021
1 parent 55032d6 commit 7b61501
Show file tree
Hide file tree
Showing 7 changed files with 638 additions and 272 deletions.
189 changes: 135 additions & 54 deletions language/move-prover/doc/paper21/analysis.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,43 @@

\Paragraph{Predictability and Performance Improvements}

Compared to the version of the Move Prover which was released in September 2020
as part of version 1.0 of the Diem project we observe many improvements in
verification speed and predictability of verification outcome, which we track
back to the bytecode transformations we have described here. These results are,
however, not so easy to quantify, as the Move language has evolved and sources
written today are not compatible with sources this time back. Moreover, the Diem
framework and its specification, which is the basis of our benchmarking, has
evolved as well, adding more functionality and tighter specifications.

As one data point we use the |DiemAccount| module, the biggest module in the
Diem framework. This module encapsulates basic functionality to create and
The three improvements described above resulted in a major qualitative
change in performance and reliability. In the version of \MVP released
in September 2020, correct examples verified fairly quickly and
reliably. But that is because we needed speed and reliability, so we
disabled some properties that always timed out and others that timed
out unpredictably when there were small changes in the framework. We
learned that incorrect programs or specifications would time out
predictably enough that it was a good bet that examples that timed out
were erroneous. However, localizing the error to fix it was
\emph{very} hard, because debugging is based on a counterexample that
violates the property, and getting a counterexample requires
termination!

With each of the transformations described, we witnessed significant speedups
and, more importantly, reductions in timeouts. Monomorphization was the last
feature implemented, and, with it, timeouts almost disappeared. Although this
was the most important improvement in practice, it is difficult to quantify
because there have been many changes in Diem framework, its specifications,
\MVP, and even the Move language over that time.

%% Compared to the version of the Move Prover which was released in September 2020
%% as part of version 1.0 of the Diem project we observe many improvements in
%% verification speed and predictability of verification outcome, which we track
%% back to the bytecode transformations we have described here. These results are,
%% however, not so easy to quantify, as the Move language has evolved and sources
%% written today are not compatible with sources this time back. Moreover, the Diem
%% framework and its specification, which is the basis of our benchmarking, has
%% evolved as well, adding more functionality and tighter specifications.

It is simpler (but less important) to quantify the changes in run time of \MVP
on one of our more challenging modules,
%% As one data point we use
the |DiemAccount| module, which is the biggest module in the
Diem framework. This module implements basic functionality to create and
maintain multiple types of accounts on the blockchain, as well as manage their
coin balances. It was called |LibraAccount| in release 1.0 of \MVP. The below
table lists the number of lines, functions, invariants, conditions (requires, ensures,
coin balances. It was called |LibraAccount| in release 1.0 of \MVP. The table
below lists the number of lines, functions, invariants, conditions (requires, ensures,
and aborts-if), as well as the verification times:

{
Expand All @@ -33,35 +56,58 @@
\vspace{2ex}
}

\TODO{Dave}{Can we say how many specifications were disabled?}

\noindent Notice that |DiemAccount| has significantly grown in size compared to
|LibraAccount|. Specifically, additional specifications have been
added. Moreover, in the original |LibraAccount|, some of the most complex
functions had to be disabled for verification because the old version of \MVP
would timeout on them. In contrast, in |DiemAccount| and with the new version,
all functions are verified. Nevertheless, verification time has been improved by
roughly 30\%, in the presence of 3x more global invariants, and .5x more
would time out on them. In contrast, in |DiemAccount| and with the new version,
all functions are verified. Verification time has been improved by
roughly 30\%, in the presence of three times more global invariants, and 50\% more
function conditions.

We were able to observe similar improvements for the remaining of the 40 modules
of the Diem framework. All of the roughly 1/2 dozen timeouts in verification in
of the Diem framework. All of the roughly half-dozen timeouts in verification in
the framework resolved after introduction of the transformations described in
this paper. Also, specifications which were introduced after the new
transformations did not introduce new timeouts. A further improvement is that
often, in cases where specification and program disagree, a timeout occurred
which went away only after fixing the spec or the code, making debugging of such
verification failures rather hard. This problem also disappeared.
transformations did not introduce new timeouts.

%% A further improvement is that
%% often, in cases where specification and program disagree, a timeout occurred
%% which went away only after fixing the spec or the code, making debugging of such
%% verification failures rather hard. This problem also disappeared.


\Paragraph{Causes for the Improvements}

It is hard to clearly identify the reasons for improvements when dealing with
heuristic systems like SMT solvers. Moreover, besides of the transformations
described in this paper, many more smaller changes had been made to \MVP,
including micro-tuning the SMT encoding of the verification problem in
Boogie. Tracking the causes of improvements incrementally was not the highest
priority of our work.
It's difficult to pin down and measure exactly why the three transformations
described improved performance and reliability so dramatically.
We have explained some reasons in the subsections above: the alias-free memory model
reduced search through combinatorial sharing arrangments, and the
fine-grained invariant checking results in simpler formulas for the SMT solver.
We believe that one reason is just that the translated SMT formulas are simpler.

We found that most timeouts in specifications stemmed from our liberal
use of quantifiers. To disprove a property $P_0$ after assuming a
list of properties, $P_1, \ldots p_n$, the SMT solver must show that
$\neg P_0 \wedge P_1 \wedge \ldots \wedge P_n$ is satisfiable. The
search usually involves instantiating universal quantifiers in $P_1,
\ldots, P_n$. The SMT solver can do this endlessly, resulting in a
timeout. Indeed, we often found that proving a post-condition |false|
would time out, because the SMT solver was instantiating quantifiers
to find a satisfying assignment of $P_1 \wedge \ldots \wedge P_n$.
Simpler formulas result in fewer intermediate terms during solving,
resulting in fewer opportunities to instantiate quantified formulas.

%% It is hard to clearly identify the reasons for improvements when dealing with
%% heuristic systems like SMT solvers. Moreover, besides of the transformations
%% described in this paper, many more smaller changes had been made to \MVP,
%% including micro-tuning the SMT encoding of the verification problem in
%% Boogie. Tracking the causes of improvements incrementally was not the highest
%% priority of our work.

Nevertheless, we believe that one of the biggest impacts, specifically regards
We believe that one of the biggest impacts, specifically regards
removal of timeouts and predictability of verification, is monomorphization. The
reason for this is that monomorphization allows a multi-sorted representation
of values in Boogie (and eventually the SMT solver). In contrast, before
Expand Down Expand Up @@ -113,6 +159,9 @@
well as the borrow semantics which enables optimizations like reference
elimination (Sec.~\ref{sec:RefElim}).

\TODO{Dave}{\textbf{Junkil:} Some definitions were missing from the prelude, like \solidity, so
I added some definitions, but they may not be what you wanted.}

In contrast to the other approaches that only focus on specific vulnerability patterns~\cite{mythril,oyente,maian,securify}, \MVP offers the rich specification language based on program logic, thus allowing users to define the specifications of their contracts.
As regards expressiveness of specification, to the best of our knowledge, no
existing specification approach for smart contracts based on inductive Hoare
Expand Down Expand Up @@ -146,32 +195,64 @@
execution, potentially obtaining higher speed for smaller data structures by
improving processor cache locality.

\Paragraph{Open Problems and Future Work}

While currently \MVP is operating to our satisfaction, there are multiple open
problems as well. For one, the set of smart contracts we are verifying still
have only medium complexity, and specifically loops are rare in the Diem
framework (loops were not discussed in this paper for reasons of space; we do
incorporate loop invariants for their verification). We anticipate the problem
of timeouts to hit us again down the road as the number of applications of \MVP
grow, and further refinement of the translation will be needed. Furthermore,
while currently there are no occurrences of false positives, we expect this problem
to hit as well.

The biggest obstacle for wider adoption, however, is seen in the complexity of
authoring and reading specifications, related to a phenomena we refer to as
``specification boilerplate''. Pre/post condition specifications are often
verbose and difficult to read and write. At the time of this writing, function
specifications in the Diem framework are often of similar size than function
implementations. A common problem is also sharing between aspects of specifications:
for example, if function |f| calls function |g| and the later function aborts, the
aborts condition propagates from |g| to the caller |f|. While the Move specification
language has mechanisms to express this kind of sharing by referring to the aborts
condition of |g| in the specification of |f|, this mechanism also makes specifications
less readable, and leaks implementation details into the specification of |f|.
We are currently experimenting with multiple strategies to cope with this, ranging
from a better methodology and language support to structure specifications, to
automatically inferring specs for some functions.
\Paragraph{Future Work}

%% DD Note: I'm taking a less specific and longer-term view of future work.
%% This is all a matter of taste, so feel free to go back to the previous
%% version if you prefer.

\MVP is conceived as a tool for achieving higher assurance systems,
not as a bug hunting tool. Having at least temporarily achieved
satsifactory performance and reliability, we are turning our attention
to the question of the goal of higher assurance, which raises several
issues. If we're striving for high assurance, it would be great to be
able to measure progress towards that goal.
Since system requirements
often stem from external business and regulatory needs, lightweight
processes for exposing those requirements so we know what needs to be
formally specified would be highly desirable.

As with many other systems, it is too hard to write high-quality
specifications. Our current specifications are more verbose than they
need to be, and we are working to require less detailed
specifications, especially for individual functions. We could expand
the usefulness of \MVP for programmers if we could make it possible
for them to derive value from simple reusable specifications.
Finally, software tools for assessing the consistency and completeness
of formal specifications would reduce the risk of missing bugs because
of specification errors.

However, as more complex smart contracts are written and as more
people write specifications, we expect that the inherent computational
difficulty of solving logic problems will reappear, and there will be
more opportunities for improving performance and reliability. In addition
to translation techniques, it will be necessary to identify opportunities
to improve SMT solvers for the particular kinds of problems we generate.

%% While currently \MVP is performing to our satisfaction, there are multiple open
%% problems as well. For one, the set of smart contracts we are verifying still
%% have only medium complexity, and specifically loops are rare in the Diem
%% framework (loops were not discussed in this paper for reasons of space; we do
%% incorporate loop invariants for their verification). We anticipate the problem
%% of timeouts to hit us again down the road as the number of applications of \MVP
%% grow, and further refinement of the translation will be needed. Furthermore,
%% while currently there are no occurrences of false positives, we expect this problem
%% to hit as well.

%% The biggest obstacle for wider adoption, however, is seen in the complexity of
%% authoring and reading specifications, related to a phenomena we refer to as
%% ``specification boilerplate''. Pre/post condition specifications are often
%% verbose and difficult to read and write. At the time of this writing, function
%% specifications in the Diem framework are often of similar size than function
%% implementations. A common problem is also sharing between aspects of specifications:
%% for example, if function |f| calls function |g| and the later function aborts, the
%% aborts condition propagates from |g| to the caller |f|. While the Move specification
%% language has mechanisms to express this kind of sharing by referring to the aborts
%% condition of |g| in the specification of |f|, this mechanism also makes specifications
%% less readable, and leaks implementation details into the specification of |f|.
%% We are currently experimenting with multiple strategies to cope with this, ranging
%% from a better methodology and language support to structure specifications, to
%% automatically inferring specs for some functions.



Expand Down
Loading

0 comments on commit 7b61501

Please sign in to comment.