The Assembler 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 - The TVM Assembler.
The present contest covers the Phase 1 Verification of The Assembler - 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 behaviour 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.
System Artifacts
The Assembler module to be specified is located in the following repositories:
Name
Repository
Branch
Hash
Assembler
master
60e5d3aff02aa5c0aba8061b6a3a96ad02e46ef9
Types
master
e0ce6c625ba86f599f5d27a41990007b27400c07
Contest dates
Nov 11, 21 - Nov 30, 21
Voting time
7 days
Rewards
The total contest budget is 168 kTON, whereby 85% are allocated to the contestant awards and 15% are allocated to the jury reward.
The contestant awards are distributed as follows:
Place 1 - 75 kTON
Place 2 - 45 kTON
Place 3 - 22.5 kTON
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 total budget for jury rewards is 15% of the above-mentioned contest reward budget (18 kTON).
This amount shall be distributed between jurors who have voted and provided feedback on submissions.
The proportion of the total budget assigned to a juror shall be defined according to the extent of this jurorâs participation in the contest, i.e. the count of votes cast by this juror divided by the total votes cast count for this contest.
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.