sys

SYS：良好な（ブラウザー）コードで良好なバグを見つけるための静的/シンボリックツール

興味があるなら、ここで（非常に）新しい再実装をチェックしてください！

インストール

依存関係をインストールします

sysをローカルにインストールする場合：

• LLVM-9、LLVM-9-Tools
• --sharedオプションで構成されたブレクター。クローン後のブレクターをインストールする方法の例として、このファイルのbuild()およびpackage()関数を参照してください。 Arch Linuxでは、AURからboolector-gitをインストールできます。
• Haskellツールスタック

または、Ralf-Philipp WeinmannのDockerfileを使用できます。

プロジェクトを構築します

すべての依存関係をインストールしたら、ツールを構築できるはずです。

 stack build

テスト

ツールを構築したら、テストを構築して実行できます。

 stack test

これにより、テストスイートの多かれ少なかれフルバージョンと、ペーパーにリストされているすべてのバグの回帰テストが実行されます。スイートは、64GBのRAMと8つのスレッドを備えたラップトップで2分強かかります。 1つの例外を伴うすべてのテスト---ソースが追跡するのに苦労しているバグ---は渡す必要があります。他に失敗した場合は、テストを再実行してみてください。ソルバーはタイムアウトした可能性があります（これはマシンでは発生していませんが、匿名性のためのログインを提供できないため、マシンで発生する可能性があります）。

紙の結果を再現したい場合は、他に何もない場合は、実行してください。

 stack test --ta '-p End-to-end'

走る

ツールを構築したら、それを使用してバグを見つけることができます！

 stack exec sys

ツールにはいくつかのオプションが必要です。

  -d DIR    --libdir=DIR   directory (or file) to analyze
  -e EXTN   --extn=EXTN    file extension
  -c CHECK  --check=CHECK  checker to run

• -dオプションは、ディレクトリ（LLVMファイルを含む）または単一のLLVMファイルを指定するために使用されます。
• -eオプションは、チェックするファイルの拡張機能を指定するために使用されます。これは、さまざまな最適化レベルでプロジェクトを構築するときに役立ちます（例： -O0および.ll-O0_p .ll-O0 o0_pを生産用にデバッグビルド用に.ll-o0）。
  • llすべての*.llファイルと一致します
  • O0すべて*.ll-O0および*.ll-O0_pファイルに一致します
  • O1すべて*.ll-O1および*.ll-O1_pファイルに一致します
  • O2すべて*.ll-O2および*.ll-O2_pファイルに一致します
  • O3すべて*.ll-O3および*.ll-O3_pファイルに一致します
  • Ogすべて*.ll-Ogおよび*.ll-Og_pファイルに一致します
  • Osすべて*.ll-Osおよび*.ll-Os_pファイルと一致します
  • Ozすべて*.ll-Ozおよび*.ll-Os_zファイルに一致します
  • prodすべての*_pファイルと一致します
  • すべてのファイルと一致しany
• -cオプションは、実行するチェッカーを指定するために使用されます。
  • uninit ：初期化されたメモリチェッカー
  • heapoob ：MALLOC OOBチェッカー
  • concroob ：ネガティブインデックスOOBチェッカー
  • userinput ：ユーザー入力チェッカー

例

FirefoxのPRIOライブラリで私たちのツールが見つかった初期化されたメモリアクセスバグを見つけるには：

 $ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p

ツールは2つのバグにフラグを立てます。最初を見てみましょう：

 Stack uninit bug
Name "serial_read_mp_array_73"
in 
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]

serial_read_mp_array（）関数を検査すると、バギーブロックパスは%4 （最初のブロック）から%71から、[ %73 ]です。

ヘルプ

Arch Linux以外の何もテストしていません（おそらくテストしません）。ただし、他のOSのサポートを追加し、システムを構築するパッチを統合させていただきます！

ディレクトリ構造

 ├── app            -- Executable used to run the checkers
├── src
│   ├── Checkers   -- Static and symbolic checkers
│   ├── Control    -- Logging helpers
│   ├── LLVMAST    -- LLVM AST interface
│   ├── InternalIR -- Internal IR used to represent paths for both static and symex
│   ├── Static     -- Static checker DSL
│   └── Symex      -- Symbolic DSL and execution engine
├── community      -- Community files
└── test           -- Tests