Silver: Smart contract static analyzer and formal verifier

Running the verifier on the Multiply contract method

logo

Inspiration

Security and correctness are paramount when developing smart contracts. Smart contracts are vulnerable to many kinds of securty vulnerabilties and bugs e.g. recently a bug in the OpenSea Ethereum dApp allowed NFTS to be sold well below their owners current listing prices resulting in six-figure losses. The open, immutable nature of smart contracts that deal with financial assets makes them inviting targets for attackers. Both deliberate attacks and inadvertent errors by developers unfamiliar with blockchain tech can result in costly losses for an organization in terms of money and reputation.

Ethereum has a large array of static analysis and formal verification tools and formal verification of Ethereum smart contracts is an active area of research both by the Ethereum team and outside contributors and companies like Microsoft with their Verisol tool for verifying Solidity code. Companies like Certik actively pursue research into formal verification languages for smart contracts like DeepSEA. If Stratis is to be competitive it should start developing its own eco-system of static analysis and formal verification tools.

Stratis is unique in that it uses the .NET CLR for its smart contract VM instead of a bespoke VM like the EVM. This has both advantages and disadvantages. VMs like the .NET CLR and Java's JVM and languages like C# and Java are undoubtedly more complex than special-purpose VMs like the EVM and lanuages like Solidity. However the .NET CLR and C# are used by millions of developers and have been studied for decades with the resources of a billion-dollar company behind efforts to find vulnerabilities and secure the enterprise and business applications that depend on them. An experienced C# developer has a better chance at writing good smart contract code for the CLR compared to using an unfamiliar language like Solidity. Languages like Certik's DeepSEA designed to support formal verification present a hurdle of unfamiliarity that makes them inaccessible to many developers.

The original goal of Stratis was to make blockchain programming accessible to the millions of developers who rely on C# and .NET today by removing the need to master another programming language. Silver is a project to also make techniques for secure smart contract development and auditing like static analysis and formal verification accessible to C# and .NET developers in an open-source library that can provide a viable alternative to commercial closed-source propietary tech used in services provided by companies like Certik.

What it does

Silver is a static analyzer and formal verifier for Stratis smart contracts. Silver works both at the source code level and the bytecode level to provide knowledge about smart contract code and potential vulnerabilities and provide logical guarantees about smart contract code behavior before it runs.

The existing validators in the Stratis SCT tool for smart contracts examine the .NET types, type members, and CIL instructions of a contract. This doesn't analyze the behavior or logic of a contract e.g. contracts that are re-entrant and call themselves before completely updating the world state can be a source of exploits. There are all kinds of pitfalls in smart contract programming that aren't detectable at the type and instruction level. Right now Stratis relies on human review, unit tests, and whitelisting contracts for determining if a smart contract has bugs or security vulnerabilities. This process is fallible and doesn't scale and centralizes the control of smart contract deployment which goes against the ethos of blockchain tech. The existing SCT validation tool is not integrated into Visual Studio and must be run externally from the command-line which makes a sub-optimal development experience.

Silver is a tool that can support existing methods of smart contract validation by providing knowledge and insight in smart contract code. The Silver static analyzer analyzes C# code at design-time in Visual Studio via a Roslyn diagnostic analyzer and provides immediate feedback to developers about problems it detects. Silver can also analyze .NET CIL code in a bytecode assembly via a command-line interface before it is deployed and does standard static analysis like call-graph, control flow, dataflow, point-to and taint analysis on the methods in a contract. Many of these analyzer work best with graphs as output and Silver can output graphs in a variety of formats including DGML which has integrated support inside Visual Studio.

The Silver formal verifier allows developers to embed annotations in C# code that specified pre-conditions, post-conditions, and invariants for methods and classes and translates this code to the Boogie language which can then be verified by the Boogie program verifier.

Silver tools are designed to be fully integrated into Visual Studio and the C# language giving users immediate notification on feedback on tasks and potential problems. For enterprise blockchain developers, Silver can simplify and accelerate the development of smart contracts in C# by providing visual validation and analysis of their code right inside Visual Studio as they are writing it without having to run an external command-line tool for validation after building their project. For administrators and DevOps types Silver can provide visibility and insight into the smart contract CIL code that is deployed and executed as part of their decentralized apps, and any vulnerabilities that may be present.

How it works

The Silver static analyzer for CIL is based on the terrific analysis-net project which I forked to make a .NET 6.0 branch This project depends on Microsofts Common Compiler Infrastructure which is the precursor to Mono Cecil and still a very capable static analysis tool. The Silver static analyzer loads a .NET assembly where the instructions are translated by analysis-net to a three-address code format which makes it more suitable for analysis. analysis-net provides many different kinds of analysis for .NET CIL code and the output can be saved to DGML format graphs which can be opened and viewed inside Visual Studio.

The Silver formal verifier rewrites and compiles C# smart contracts using the Spec# compiler. Silver contains a version of the smart contracts base library that can be consumed by Spec#. To verify a smart contract library, Silver takes the C# code, rewrites it to be consumed with Spec# and then compiles it using the Spec# compiler.

All the specifications in the contract are then statically checked to see if they are satisfied. None of the Spec# code is deployed or used at runtime...the assembly the Spec# compiler produced is only used for verification and is kept separate from the regular smart contract assembly which is compiled normally using MSBuild. The --verify flag tells Silver to cattempt verification of the smart contract code using Spec#.

For example the simple Multiply contract takes 2 integers and multiplies them. In the C# code we insert comments that begin with \\@ which contain our specification:

using Stratis.SmartContracts;
[Deploy]
public class MultiplyContract : SmartContract
{
    public MultiplyContract(ISmartContractState state, string message)
        : base(state) {}

    public int Multiply(int x, int y)
    //@ requires 0 <= y;
    //@ requires 0 <= x;
    //@ ensures result == y * x;
        {
            int q = 0;
            int i = 0;
            while (i <= y)
            //@ invariant 0<= i;
            //@ invariant i<= y;
            //@ invariant q == (i * x);
            {
                //@ assert  q == (i * x);
                //@ assert  q + x == (i * x) + x;
                q = q + x;

                //@ assert  q == (i * x) + x;
                //assumption needed for distribution of operators.
                //@ assume (i*x) + x == (i+1) * x;
                //@ assert  q == (i+1) * x;
                i = i + 1;
                //@ assert  q == i * x;
            }
            //@ assert  q == i * x && i == y;
            return q;
        }
}

Note that all of the specs aren't necessay, ths example just shows what kind of specifications can be wriiten and that the syntax of specifications is just C#. We can compile this project using Silver with the --verify flag to also create a Spec# assembly.

The compiler will warn us if any of the specs fail. The verify command invokes the Boogie program verifier on the assembly we created and lets us see the details.

We made a mistake in our Multiply algorithm. The invariant on line 18 that in the body of the loop it is always i <= y does not hold because i gets incremented inside the loop down at the bottom even though our loop condition says i <= y.

These kinds of off-by-1 errors are extremely common in programming but can be disastrous in a smart contract. If we had a SendMoney contract method like

public void SendMoney(int c, int d, Address recep)
    {
        int r = Multiply(c, d);
    }

We would see that the method pre-conditions fails to hold because the variable c could be a negative number. . If we put checks in our SendMoney method

public void SendMoney(int c, int d, Address recep)
    {
        if (c >= 0 && d >= 0)
        {
            int r = Multiply(c, d);
        }
    }

The verification completes without errors.

Accomplishments that we're proud of

I didn't know anything about blockchain tech till this hackathon and Stratis is a really interesting project that makes blockchain development accessible to me. This project has a lot of moving parts that needed to fit together and I learned a great deal in doing it