Silver

About

Silver is a static analysis and formal verification tool for Stratis smart contracts. Silver can analyze both C# source code using a Roslyn diagnostic analyzer and CIL code in a .NET bytecode assembly and can run both inside Visual Studio and on the command line.

Silver can validate C# code using a Roslyn diagnostic analyzer according to the same rules for types and members used by the Stratis CLR VM for smart contracts. All the validation policies currently in use will be ported to the Roslyn analyzer.

Silver can disassemble smart contract CIL code in a .NET bytecode assembly:

and statically analyze it using the Analysis.Net framework e.g. the following is a call-graph analysis of the methods in the Address Mapper contract.

Silver can output graphs in different formats like PNG images:

or in the DGML format which are natively supported in Visual Studio:

Silver can formally verify smart contracts in C# using the Spec# compiler from Microsoft Research:

See the wiki for more in-depth technical information and documentation.

Building

Requirements

• NET 6.0
• Mono (on *nix/MacOs)
• libgdiplus (on *nix/MacOs, for graph drawing)

Known issues

The verifier is currently broken on non-Windows as the Spec# verifier depends on some Windows specific code in the compiler to write .PDB files which are needed to verify an assembly. Everything else should work cross-platform including the analyzers and compiler.

Steps

1. Ensure requirements are installed
2. Clone this git repo and submodules: git clone https://github.com/allisterb/Silver.git --recurse-submodules
3. Run ./build or build.cmd in the root repo directory. Build should complete without errors.
4. Run ./silver install to download and install the external tools needed.
5. Compile and analyze one of the example projects e.g. ./silver compile examples\AddressMapper\AddressMapper.csproj and silver dis examples/AddressMapper/bin/Debug/netcoreapp2.1/AddressMapper.dll
6. On Windows you can verify one of the example projects e.g. silver verify examples\SimpleVerifiableContracts\SimpleVerifiableContracts.csproj or silver compile examples\SimpleVerifiableContracts\SimpleVerifiableContracts.csproj --verify

Usage

See silver help for the different commands and actions.