drmathias/silver

Static analyzer and formal verifier for Stratis smart contracts

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 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. In the screenshot above the class generates a diagnostic with the code SC0002 when a smart contract class does not inherit from the base Stratis.SmartContracts.SmartContract class. All the validation policies currently in use will be ported to the Roslyn analyzer.

Silver can also statically analyze CIL code in a .NET assembly using the Analysis.Net framework e.g. the following shows a call-graph analysis of the methods in the Address Mapper contract.

Silver can output graphs in different formats like PNG images.

Silver can also generate graphs in the DGML format which are natively supported in Visual Studio. The following screenshot shows the call-graph in DGML format being manipulated and analyzed by the Visual Studio DGML editor.

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 compile and verify one of the example projects e.g. ./silver compile examples\AddressMapper\AddressMapper.csproj --verify and silver verify examples\AddressMapper\bin\Debug\netcoreapp2.1\ssc\AddressMapper.dll

Usage

See silver help for the different commands and actions.