Skip to content

Commit

Permalink
Add paragraph about conclusive result validating base hypothesis
Browse files Browse the repository at this point in the history
...regarding the usefulness of running pre-existing tests
by leveraging symbolic execution means offered by klee
in the context of smart contract quality assurance testing
  • Loading branch information
thierrymarianne committed Nov 17, 2021
1 parent 0e00e40 commit 97523d1
Showing 1 changed file with 10 additions and 1 deletion.
11 changes: 10 additions & 1 deletion docs/30-latest-mvp-for-safepkt-smart-contract-verifier.md
Original file line number Diff line number Diff line change
Expand Up @@ -259,6 +259,16 @@ See this issue from project-oak/rvt about [`cargo veriy` being incompatible with
- Port of the verifier as an extension for [Jetbrains products](https://plugins.jetbrains.com/docs/intellij/getting-started.html)
- Port of the verifier as a [Sonarqube plugin](https://docs.sonarqube.org/latest/extend/developing-plugin/)

### Conclusive results

The default branch (`buggy-smart-contract`) available from SafePKT smart contract example,
offers a clear demonstration of how to leverage SafePKT verification tools,
in order to discover issues with a rust-based Smart Contract.

The smart contract example here is based on [ERC20 technical standard](https://fr.wikipedia.org/wiki/ERC20),
and can be found in the following repository:
https://github.com/LedgerProject/safepkt_smart-contract-example

## System stability, maintainability

### Installation
Expand All @@ -280,7 +290,6 @@ A working strategy consists in ensuring that
- `rvt` belongs to [`docker` group](https://docs.docker.com/engine/install/linux-postinstall/)
- `www-data` is the user running the nginx instance


### Ballpark performance

As of today, the verification process takes about 90s when executed from our dedicated server for a suite of about 30 tests without fuzzing.
Expand Down

0 comments on commit 97523d1

Please sign in to comment.