/Static-Module-Verifier

Static Module Verifier technology enables full module analysis using Microsoft Azure.

Primary LanguageC#MIT LicenseMIT

Static Module Verifier

Static Module Verifier enables two things at it's core:

  • Building IR for a module to perform full program analysis
  • Scaling the analysis using the Azure cloud

StaticModuleVerifier supports multiple build environments, and can produce IR based on any toolchain that you specify. Examples of such toolchains are the [SMACK] (https://github.com/smackers/smack/) toolchain and the [SLAM] (https://www.microsoft.com/en-us/research/project/slam/) toolchain, which is also used as the frontend in the [Static Driver Verifier] (https://msdn.microsoft.com/en-us/library/windows/hardware/ff552808(v=vs.85).aspx) project.

StaticModuleVerifier takes as input a configuration file that specifies the series of actions to execute for building, intercepting, and then performing analysis. Details of the configurations can be found in the documentation folder.

Build

Windows

  • Prerequisites:
    • Visual Studio 2015
    • Microsoft Azure SDK for VS 2015: version 2.9 .NET
    • NuGet with default configurations
  • After cloning, you should be able to open the smv.sln file in your repository in VS2015
  • The smv.sln solution should build in VS2015

Linux

  • Prerequisites
    • Mono complete installation
    • NuGet for Linux
  • After cloning, you will need to install the following packages
    • nuget install Microsoft.Data.Edm WindowsAzure.ServiceBus WindowsAzure.Storage WindowsAzure.ServiceBus
    • nuget install WindowsAzure.WindowsAzure.ServiceRuntime WindowsAzure.ServiceBus AzureSDK2.2DLLs WindowsAzure.Storage
    • nuget install WindowsAzure.Storage WindowsAzure.Storage -Version 4.3.0 WindowsAzure.ServiceBus -Version 3.0.0-preview -Pre
    • nuget install WindowsAzure.ServiceBus -Version 3.0.0
    • Note that nuget will place them in the current working directory. It is suggested that you create a packages folder and run nuget within that folder to have the packages be centrally located.
  • Edit the following files and make sure the Azure references point to the correct locations (hintpaths):
    • SMVActionsTable/SMVActionsTable.csproj
    • SmvCloudWorker/SmvCloudWorker.csproj
    • SmvLibrary/SmvLibrary.csproj
    • SmvSkeleton/SmvSkeleton.csproj
  • Now you should be able to do xbuild at the top level to build smv.sln

Usage

Packaging

StaticModuleVerifier expects the following directory structure for plugins:

  • bin: all StaticModuleVerifier core binaries are placed here (including external dependencies)
  • analysisPlugins: analysis plugins are created in an analysisPlugins folder which resides at the same level as the bin folder (where you placed all the binaries).
    • bin: anlaysis plugin specific binaries (your checker etc.) and top level script for invoking StaticModuleVerifier
    • configurations: configurations that are to be used for StaticModuleVerifier.exe

The final directory structure should look as follows:

  • %SMV% (top level folder where you created your deployment)
    • bin: contains all binaries, and today, the intercept.xml as well
    • analysisPlugins: contains sub folders that have analysis plugins
      • SDV: Static Driver Verifier analysis plugin
      • bin: binaries that are SDV specific. Usually also a cmd script that wraps calls to smv.exe
      • configurations: StaticModuleVerifier configurations for build and analysis
      • other folders can be created as necessary

Plugin

Coming soon...

Interception

Coming Soon...

SMV and the Azure Cloud

  • Deploying to Azure
    • You will need a valid subscription for Azure
    • You will need to create the following:
      • Storage service with your name of choice (for example, MySmvCloud)
        • Create the following containers: smvversions, smvactions, smvresults
      • Service bus with the same name as the service (MySmvCloud) and a queue called smvactions
      • Cloud service with same name as the service (MySmvCloud)
      • Queue named smvactions
    • Edit the following files for the connection strings for your newly created services:
      • SmvCloud\ServiceConfiguration.Cloud.cscfg
      • SmvLibrary\CloudConfig.xml
      • SmvCloudWorkerContent\CloudConfig.xml
  • After creating your deployments
  • To use the cloud, you can add executeOn="cloud" to any analysis action node in your configurations, and it will execute using the SMV cloud

Miscellaneous tools

  • Azure Storage Explorer for viewing storage accounts and their contents