Giter Club home page Giter Club logo

static-module-verifier's Introduction

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

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

static-module-verifier's People

Contributors

abhimohta avatar dependabot[bot] avatar microsoft-github-policy-service[bot] avatar nated-msft avatar rahulku avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar

static-module-verifier's Issues

SMV Cloud: 404 14 times in a row

We have come to accept a certain failure rate from SMV Cloud due to coordination with Azure back end issues. At this moment we can handle this thru an external rerun mechanism.

However once in a while SMV Cloud repeatedly fails the same driver with a 404. Last week I ran two PTPs with a max rerun of 5. That was not enough. This weekend I did a max rerun of 20. One driver kept failing up to the 14th rerun / 36th hour where I then ran out of patience. This means rerun approach does not work. The fix should either be to eliminative any code that would reuse state/tokens/guids for same driver between reruns. Alternatively a reduction of likelihood that we hit 404s.

The failing folder is here: \redmond\osg\Threshold\Tools\CORE\SiGMa\DPlat-DQT\Share\JakobL\Public\2017-03-31-SMVCloud404times14\win8_rtm_drivers_input_mouser\

The svb.log file shows 14 times:

[FATAL ERROR] Microsoft.WindowsAzure.Storage.StorageException : The remote server returned an error : (404) Not Found. ---> System.Net.WebException: The remote server returned an error: (404) Not Found. [C:\slam1\WDK\win8_rtm\drivers\input\mouser\mydriver.vcxproj]

Feature Request: Command should log exit value

Here is an example

When reviewing the SMV log (generated with /debug) I see:

[INFO] Launching copy with arguments: "J:\SD\slam\5\sdv\product\osmodel\osmodel.c" "J:\SD\slam\5\WDK\win8_rtm\admin\wmi\ipmi\driver\lib\sdv\sdv-harness.c"
...
J:\SD\slam\5\WDK\win8_rtm\admin\wmi\ipmi\driver\lib>copy "J:\SD\slam\5\sdv\product\osmodel\osmodel.c" "J:\SD\slam\5\WDK\win8_rtm\admin\wmi\ipmi\driver\lib\sdv\sdv-harness.c"
...
The system cannot find the file specified.

Request: It would be great if additionally SMV could echo the error level that the Command exited with.

avn hangs from time to time

Sometimes avn just hangs there forever. Here is an example output,

E:\linux\drivers\media_v4l2core>avn media-v4l2-core-null.inst.bpl /cloud
[INFO] Running using cloud...
[INFO] SMVFastAVN initialized.
[INFO] Using cloud.
[INFO] Validating XML against schema: e:\smv-fastavn-11-7-2016\bin\Config.xsd
[INFO] Running local scheduler with 4 threads
[INFO] Validating XML against schema: e:\smv-fastavn-11-7-2016\bin\CloudConfig.xsd
[INFO] Scheduler Instance GUID: 2e5627ad-4368-4e35-b4df-4c538e466b20
[INFO] Using plugin FastAVN.SMVFastAVN for analysis.
15 of 862 jobs remaining. Avg(s): 89.13. Std.Dev(s): 240.58[ERROR] Failed to complete action: e4863264-bfd3-4c74-ab7b-4cea1985fe04 (CheckEntryPoints)
12 of 862 jobs remaining. Avg(s): 97.47. Std.Dev(s): 295.36[ERROR] Failed to complete action: ee3ed645-3c49-4c2b-8305-54d6016e9e48 (CheckEntryPoints)
6 of 862 jobs remaining. Avg(s): 111.08. Std.Dev(s): 347.75[ERROR] Failed to complete action: aea26428-6f5f-4349-b0e5-64a588a9622b (CheckEntryPoints)
[ERROR] Failed to complete action: 0069e28a-a7fb-4538-96c8-cce5d72a3ded (CheckEntryPoints)
0 of 862 jobs remaining. Avg(s): 125.97. Std.Dev(s): 411.19
-2 of 862 jobs remaining. Avg(s): 134.12. Std.Dev(s): 444.05

I have to kill the process and run fastavn to merge bugs manually.

Shaobo

Bug: msbuild Build error does not lead to SMV failing verification

Without fix for Bug VSO 9798617 (SMV: ITP: Regression: win8_rtm\net\netio\directaccess\danlb\sys) we have the intercepted build failing.

The evidence is in sdv\smvcl.log:

J:\SD\slam\5\WDK\win8_rtm\net\netio\directaccess\danlb\sys\sdv\headers\ndis.h(5): fatal error C1083: Cannot open include file: 'J:\SD\slam\5\sdv\product\osmodel\wdm\sdv_ndis.h': No such file or directory

Expected: SMV catch this msbuild error and stops verification.

Actual: SMV does not catch this build error. Verification proceed with scan step.

SMV-SDV: Provide wlimit style protection of all started processes

This is a large feature request. It would however be a strong foundational improvement to SMV.

What:

  1. Wrap all processes in a job.
  2. By default prevent processes "escaping".
  3. Provide knobs to control limits on various resources: wall clock time, space, user time. Knobs would be accessible thru xml tags I would imagine.
  4. Provide resource statistics upon job completion.

When:
For build, intercepted build and verification. Really any calls to "exec".

How:
I would be open to expose a wlimit API as a managed dll. This dll would essentially provide a replacement of "exec". Next step would be to call this from SMV and additionally expose the most useful knobs as XML.

SMV Cloud: SMV saw an error yet still return error code 0

Hi Rahul.

I ran two PTPs on two separate machines. On both machines I see sporadic examples of errors from the Azure layer yet SMV returns 0 indicating a succesful run.

Fix suggested is trivial: Change regular error to a "Fatal error". Or at least make sure an error results in a non-zero exit code from SMV.

Here is a specific example:
+++
robocopy /mir /nfl /ndl C:\slam1\WDK\src_5239\fail_drivers\kmdf\fail_driver3\driver \redmond\osg\Threshold\Tools\CORE\SiGMa\DPlat-DQT\Share\JakobL\Public\2017-04-10-smv_fatalerror_as_nonfatal
+++

Notice in svb.log you see:
+++
[INFO] 23 of 347 jobs remaining. Avg(s): 8.65. Std.Dev(s): 13.76[ERROR] Failed to complete action: 0a88c33f-6e33-4c7f-bd5c-c0debd6a2b1b (CheckRule)
...
jrerun final errorlevel 0 after 1 attempt(s).
+++

How often does this happen? In average 9.5 times per PTP.
+++
From jakobl1:
C:\slam1\WDK>findstr /m /s /c:"[ERROR] Failed to complete action" svb.log
src_5239\fail_drivers\kmdf\fail_driver3\driver\svb.log
src_5239\kmdf\fakemodem\svb.log
src_6001\input\mouser\svb.log
src_7600\storage\class\cdrom\svb.log
src_ndis\sdvmp_fail_09\svb.log
win8_rtm\drivers\wdm\1394\protocol\avc\svb.log
win8_rtm\drivers\wdm\usb\usb3\ucx\sys\driver\svb.log
win8_rtm\minkernel\storage\sbp2port\svb.log
win8_rtm\net\rras\ndis\ndproxy\svb.log
+++
From jakobl3:
K:\SD\slam\2\WDK>findstr /m /s /c:"[ERROR] Failed to complete action" svb.log
src_5239\kmdf\AMCC5933\sys\AMCC5933ISA\svb.log
src_5239\kmdf\nonpnp_fail4\svb.log
src_7600\storage\class\cdrom\svb.log
src_ndis\sdvmp_fail_30c\svb.log
src_storport\StorportMiniports\storahci\svb.log
win8_rtm\drivers\wdm\1394\protocol\avc\svb.log
win8_rtm\drivers\wdm\ir\circlass\svb.log
win8_rtm\minkernel\storage\sbp2port\svb.log
win8_rtm\net\unimodem\src\sys\modem\svb.log
win8_rtm\printscan\imaging\kernel\usbscan\winnt\svb.log
+++

SMV-AV: Redefining NT_VERIFY and procedure replication

The LI generation creates two copies of a procedure invoked within NT_VERIFY (entrypoint BdpReserveScratchVa). See email titled "Understanding the BPL" on 3/31/2017. Some context below

You can see there are two calls to BlMmFreeVirualPages (on blocks D_24 and D_30). You can also see a self loop on D_29, which I believe is SMV’s way of encoding an “assume false”. This is definitely the case that SDV (before slam.exe is run) is redefining NT_VERIFY to something else and we need to change this. But I cannot figure out where this happens. It must be in slamcl, I would guess...

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.