The Executor Module Formal Verification - Phase 1
Contest Description
In order to enhance the reliability of the platform, in this work, we propose to perform a formal verification of one the core developers system components - Node Executor.
The present contest covers the Phase 1 Verification of The Executor - The Specification.
Introduction
In the context of building high-assurance software systems, Formal Verification is a logically sound method of proving the correspondence between a provided program code and a system description, hereinafter referred to as The Specification.
The Specification contains the most important information regarding the system, such as: its general purpose, who are the users, usage scenarios, etc. Besides that, it states what kind of risks and what guarantees (if any) a system provides.
In this work, you are expected to conduct a specification on the program system in a form of well structured document. The document has to be written in the native language, maybe with sporadic mathematical notes. In our case, the document has to focus on the risks and properties that compensate those risks - it is exactly those properties that will be formally (mathematically) proven on the next
stage of quality assurance process.
The document has to be easily comprehensible both by a Business Analyst and by a Formal Verification expert.
Here, Business Analyst is a role referring to someone from the program system development team having a general comprehension of the system business logic. They are able to clarify both general system behavior and its corner cases, if any.
Specification content
The following specification content is expected to be present:
- High-level system description
-
System purpose
-
Terms of the system domain
-
Kinds of System Users
-
Architecture of the System
-
Main usage scenarios
-
Users capabilities
-
Key system algorithms
The description better be accompanied by diagrams, such as:
-
diagram of interaction between a user and a system
-
diagram of interaction between different system components
- Risks
Here, you state what main risks should be considered in the context of a system usage. For example, coins loss, ownership loss, etc.
- System Properties
In this section, you cover the following:
-
List of assumptions under which the system is expected to operate
-
Threat model
-
List of system properties, i.e. statements regarding a system behaviour in different usage scenarios
-
List of guarantees, i.e. a subset of system properties that mitigate main risks identified in the Section 2.
Assumptions convey the expected system operation conditions.
Threat model states what is expected from a perfect intruder, its capabilities, incentives, etc.
The guarantees are stated with an eye on the assumptions and the threat model.
Properties should be described mostly using terms introduced in Section 1.
The authors are free to add any kind of supplementary details enhancing the reader’s understanding even further, such as lower level function descriptions, description of abstractions used, etc. It is strongly advised to add such details only in case it adds value to the document and doesn’t clutter the main narrative.
- Appendix
Description of the most important system APIs. The system description may refer to some of those APIs to tie the explanation with the program code.
Specification Purpose
The main purpose of the specification is to provide the Formal Verification expert with enough insight on the system purpose and its expected behavior in different scenarios, so they could further perform Formal Verification of the program system.
The properties must cover the main user risks. The formulations must use well-defined described terms.
We advise to group properties by some reasonable criteria, for example by their component origin, or by the risk they eliminate.
We advise to accompany properties with mnemonic names for easier navigation and further discussion.
Specification Evaluation
The specification evaluation criteria are:
-
Logical coherence of the text
-
General conciseness: convey more with less text
-
Clarity and completeness of the system description
-
How well the risks are identified
-
Clarity and completeness of the system properties
Ideally, the specification receives a proof reading from Business Analyst before being published. The document that has been proof-read by the Аnalyst and received his/hers appreciation is expected to receive a higher score.
Generic rules
The contest should be compliant to the Generic Contest Rules.
System Artifacts
The Executor module to be specified is located in the following repositories:
| Name | Repository | Branch | Hash |
|---|---|---|---|
| Executor | https://github.com/tonlabs/ton-labs-executor | master | a28bde3e65dd35573d34e32aa4477d60162b5338 |
Contest dates
Feb 3, 22 - Feb 24, 22
Voting time
7 days
Rewards
The total award budget is 145 kEVER and distributed as follows:
- Place 1 - 75 kEVER
- Place 2 - 45 kEVER
- Place 3 - 30 kEVER
The Jury
The Jury shall be formed from acknowledged experts in the fields of security, smart contract audit, and formal verification fields, whereby:
- Jurors whose team(s) intend to provide submissions in this contest shall lose their right to vote in this contest
- Each juror shall vote by rating each submission on a scale of 0 to 10 (0 equalling rejection of the proposal); a juror may abstain from voting if they do not see themselves sufficiently qualified to judge such proposal
- A juror that has voted on a submission shall provide detailed feedback on it
Jury Guidelines
- The main goal of the jury is to check how the provided specification is accurate and full.
- The specification is intended to be understandable for an average IT professional but at the same time it must be evident it’s relatively easy to convert it to the formal one
- All the requirements mentioned above are considered as mandatory otherwise some points have to be taken from the corresponding application.
Jury Rewards
The jury reward is 1 500 EVER for each voting for each juror.
This amount shall be granted for jurors who have voted and provided feedback on all submissions.
Procedural Limitations
- Only one submission per contestant shall be accepted. Multiple submissions, including but not limited to updated versions of the initial submission, are not allowed.
- Submissions shall be made within the time frame defined above in the Contest Dates section. Late submissions shall be rejected by the Jury.
- All submissions shall contain the contestant’s contact information (preferably a Telegram ID) to ensure that the jury can match the submission to the specific contestant. If such contact information is missing, the submission shall be rejected.
- If the submission contains links to external material (reports on further work by the contestant), this material shall have the contestant’s contact details (preferably a Telegram ID), to ensure that the jury can match the material to the specific contestant. If such contact information is missing, the submission shall be rejected.
