Imagine going Skydiving. Before jumping off the plane, you will check for your parachute a hundred times, right? Checking and testing are an integral part of security; think about any security-related thing. There would likely be a mechanism of testing following afterwards, whether it is the installation of CCTV or checking the ink in pen before a written examination in school, we all follow safety measures. The higher the risk involved, the more we test things. And when we talk about smart contracts, the risk is HUGE. You cannot be careless when it comes to smart contract security.
1. Security is always needed.
You sure can lock the door twice or thrice does not matter. Can you be sure your house can’t be robbed while you are gone? You can’t because you do not know what the robber might do to break into the house—the same is true for every safety measure we take. There is no completely safe method which will guarantee safety. Still, the action we take swiftly increases our chances of being safe, which is what the game is. We want to increase the odds of being safe by employing different measures.
The world of Web3 isn’t different. There is no safe method to save yourself, but having experienced auditors from QuillAudits can increase the odds of your protocol being secured tremendously and will ensure your up-to-date security. In web3, there are two important mechanisms which help you understand how secure you are by doing some tests on your protocol:-
- Smart Contract Testing
- Formal Verification of Smart Contracts
Let’s understand them in detail and learn how they help us know our contracts’ weak points or vulnerabilities.
2. Smart Contract Testing
An experienced developer can explain the work to a machine with code. Still, sometimes the machine does not depict the exact mechanism the developer had in mind due to a flaw or a logical error in the code. Testing is the process that helps identify where our code is failing and what can be done to make it correspond with the action we need it to perform.
Smart contract testing is a phase in the development cycle in which we perform a detailed analysis of our contracts and try to find out where and why our code is failing. Almost all smart contracts undergo this phase. There are two ways smart contract testing is done. Let’s explore them.
2.1 Automated
As the name suggests, this method for testing smart contracts is used to carry out scripted testing. It involves automated software which executes repeated tests to find any vulnerabilities and defects in smart contracts. These automated testing tools can be configured with test data and expected results. Then the actual result is compared with the expected ones to check if the contract is working properly. Automated testing can be further classified into three categories.
2.1.1. Functional Testing
Suppose you write a programme to take two numbers, a and b and then return the addition of both numbers. So to check that programme, you give 2 and 8 and feed the expected result to be 10. Now when the programme runs, it should also return 10. If it does, then it works fine, and our code is correct, but if it does not, then there is some error with our code.
Functional testing requires understanding how your contract should behave in certain conditions. We can test it by running a computation with selected values and comparing the returned output. Functional Testing has three classes:-
- Unit testing:- This deals with testing individual components of the smart contract for correctness. It is assertive or requires statements on variables.
- Integration testing: – These deals with testing several individual components together. Integration testing is a level higher in the hierarchy than unit testing. It helps us determine errors arising from the interaction of different functions, which may be part of other smart contracts.
- System Testing: – This is the highest in the hierarchy. In this, we test the entire contract as one fully integrated system to see if it performs as per our needs. It is done from the user’s point of view, and the best way to do it is to deploy it on testnets.
2.1.2. Static Analysis
Static Analysis can be done without even running the programme. It involves the analysis of the source code or bytecode of the smart contract before execution. Thus giving its name, static analysis can result in the detection of some common vulnerabilities.
2.1.3. Dynamic Analysis
Unlike static analysis, dynamic analysis is carried out during the run time of the smart contracts to identify issues in code. The dynamic code analysers observe the contract’s running state and generate a detailed report of vulnerabilities and property violations. Fuzzing comes under DYnamic analysis. Fuzzing is feeding incorrect or malicious input to cause unintended code execution.
2.2 Manual
As the name suggests, this method of smart contract testing involves regular interaction with a human developer. Code audits, where developers go through lines of codes, come under the Manual mode of smart contract testing.
Manual mode requires considerable time, skill, money and effort. Still, the result is often worth it because, with this, we identify vulnerabilities that may get unnoticed in the automatic testing. There are two essential types of manual testing:-
2.2.1 Code Audits:-
The best way to test if your safety measure works properly is to try to break it. For example, if you want to check whether your car lock works properly, try to break it. Now you may ask that a skilled car thief can easily break into my car. I may not, so the solution is to hire someone adept at breaking in so that he can guide you!
Yes, I am talking about QuillAudits. We are a team of skilled auditors who can guide you. Code audits require an attacker mindset to find all possible vulnerabilities in source code. A code audit is a detailed evaluation of a smart contract’s code to uncover potential vulnerabilities and flaws.
2.2.2 Bug Bounty:-
If you think there might be some security flaws in your source code (which mostly are) and you cannot find them, you can outsource this work to freelancers by creating a reward system. It is more like announcing a reward for anyone who can hack your smart contract. By doing this, you learn about the vulnerability present in your smart contract so that you can protect it better and save your users from loss.
3. Formal Verification of Smart Contracts
Formal verification is the process of evaluating the correctness of a contract based on formal specifications. This means formal verification assesses if the code does what is intended. Formal verification uses formal methods for specifying, designing and verifying programmes.
3.1 What is the formal specification?
In the context of smart contracts, formal specifications refer to the properties which must stay the same under every possible circumstance. These are ” invariants ” properties because they cannot change and represent logical assertions about the contract’s execution.
Formal specification is a collection of statements written in formal language. Specifications cover different properties and describe how the properties of the contract should behave in other circumstances. Formal specifications are critical because if contracts fail to have invariant variables or properties change during execution, it can lead to possible property exploitation, which may lead to a huge loss.
It can help us determine whether a smart contract meets specifications or has unexpected behaviours. Formal verification has three components: a specification, a model, and a verification engine.
3.1.1 Specification
A specification is a clear, unambiguous, and complete description of the requirements for a smart contract. It should describe what the contract is supposed to do and what it is not supposed to do. Here is an example specification for a simple, smart contract that adds two numbers:
// Specification: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint)
function add(uint a, uint b) public view returns (uint) {
// Implementation details are not relevant to the specification
// …
}3.1.2 Model
A model formally represents the smart contract that can be used to reason about its behaviour. One popular model for smart contracts is the Solidity programming language. Here is an example model for the add function described above:
// Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint)
function add(uint a, uint b) public view returns (uint) {
return a + b;
}3.1.3 Verification Engine
A verification engine is a tool that can analyze a model and verify its correctness concerning a given specification. There are several verification engines available for smart contracts, including:
Mythril: an open-source symbolic execution tool that can detect a wide range of security vulnerabilities in Solidity smart contracts.
Remix IDE: an integrated development environment that includes a formal verification tool that can verify the correctness of smart contracts.
Certora Prover: a commercial tool that can verify the correctness of smart contracts using automated mathematical reasoning. Here is an example of how formal verification can be used to verify the correctness of a smart contract using the Certora Prover:
pragma solidity 0.7.6;
// Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint)
function add(uint a, uint b) public pure returns (uint) {
return a + b;
}
// Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint)
function add(uint a, uint b) public pure returns (uint) {
return a + b;
}
// Specification: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint)
function test_add(uint a, uint b) public pure returns (bool) {
uint expected = a + b;
uint actual = add(a, b);
return expected == actual;
}
// Verification: Verify the correctness of the add function
contract TestAdd {
function test_add(uint a, uint b) public view returns (bool) {
return CertoraProver.verify(test_add, a, b);
}
}In the above example, we define a Solidity smart contract that includes a model of the add function, a specification for the function, and a verification engine (Certora Prover) that can verify the correctness of the function. We also define a test function (test_add) that can be used to verify the function’s correctness.
3.2 Testing VS Formal Verification
As we discussed, testing returns the expected result for some input data bot it lacks because we cannot say about the data it hasn’t been tested on. It is practically impossible to check it on every possible input. Thus we are not sure about its “functional correctness”. That is where formal verification comes in. Formal verification methods use rigorous mathematical techniques for specifying and verifying software or smart contracts.
3.3 Techniques for formal verification
Formal verification has a wide scope of techniques for enhancing smart contract security. In this part of the blog, we will explore a few individually.
3.3.1 Model Checking
As we discussed what a formal specification is, we check the smart contract against its specification in this formal verification technique. These smart contracts are represented as state transition systems, and properties are defined using temporal logic.
This technique is primarily used to evaluate temporal properties that depict the behaviour of smart contracts over time. Access control property(admin calling selfDestruct) can be written down as formal logic. Then the model-checking algorithm can verify if the contract satisfies this formal verification.
Model checking uses a technique called State Space exploration, which is basically trying out all the possible states our smart contract can be in and then checking if any of it results in a property violation. However, this may lead to infinitely many states; hence model checkers rely on abstraction techniques to make an efficient analysis of smart contracts possible.
3.3.2 Theorem Proving
Theorem proving is about mathematical reasoning on the correctness of programmes. It deals with creating a logical impression of the contract’s system and specification and verifying the “logical equivalence” between the statements. Logical equivalence is a mathematical relationship which says that statement A is true if and only if statement B is true.
As we learned in the model checking technique, we model contracts as transition systems with finite states. Theorem proving can handle the analysis of infinite-state systems. However, an automated theorem prover cannot always know if a logical problem is decidable; thus, human assistance is often required to guide the theorem prover in deriving correctness proofs.
4. Conclusion
Testing and formal verification are both integral parts of smart contract development. These are the methods used to make smart contracts secure and help to get the contracts ready for deployment. But as you know, security is never enough. Many smart contracts were getting hacked just because there was no proper testing. Now more than ever web3 community needs more secure protocols.
We at QuillAudits are on a mission to help protect your protocols. With our skilful and experienced team, we make sure not even a single vulnerability gets unnoticed. Do visit our website and get your Web3 project secured!
