sys

SYS: Alat statis/simbolis untuk menemukan bug yang baik dalam kode yang baik (browser)

Jika Anda tertarik, lihat ulang (sangat sangat) ulang baru di sini!

Memasang

Instal dependensi

Jika Anda ingin menginstal sys secara lokal:

• LLVM-9, LLVM-9-Tools
• Boolector dikonfigurasi dengan -opsi --shared . Lihat fungsi build() dan package() dalam file ini sebagai contoh cara menginstal boolector setelah Anda mengkloningnya. Di Arch Linux, Anda bisa menginstal boolector-git dari AUR.
• Tumpukan alat haskell

Atau, Anda dapat menggunakan Dockerfile dari Ralf-Philipp Weinmann.

Membangun proyek

Setelah Anda memiliki semua dependensi yang diinstal, Anda harus hanya dapat membangun alat:

 stack build

Tes

Setelah Anda membangun alat, Anda dapat membangun dan menjalankan tes kami dengan:

 stack test

Ini akan menjalankan versi lengkap dari test suite kami, bersama dengan tes regresi untuk setiap bug yang kami daftarkan di koran. Suite ini memakan waktu lebih dari dua menit di laptop dengan RAM 64GB dan 8 utas. Semua tes dengan satu pengecualian --- Bug yang sumbernya kami kesulitan melacak --- harus lulus. Jika ada hal lain yang gagal, cobalah menjalankan kembali tesnya; Pemecah mungkin sudah waktunya (ini belum terjadi pada mesin kami, tetapi karena kami tidak dapat memberi Anda login untuk anonimitas, itu kemungkinan bahwa itu akan terjadi pada mesin Anda).

Jika Anda hanya ingin mereproduksi hasil kertas dan tidak ada yang lain, jalankan:

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

Berlari

Setelah Anda membangun alat, Anda sekarang dapat menggunakannya untuk menemukan bug!

 stack exec sys

Alat ini mengambil beberapa opsi:

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

• Opsi -d digunakan untuk menentukan direktori (berisi file LLVM) atau file LLVM tunggal.
• Opsi -e digunakan untuk menentukan ekstensi file yang akan diperiksa. Ini berguna saat membangun proyek Anda dengan tingkat optimisasi yang berbeda (misalnya .ll-O0 untuk pembuatan debug dengan -O0 dan .ll-O0_p untuk produksi).
  • ll mencocokkan semua file *.ll
  • O0 mencocokkan semua file *.ll-O0 dan *.ll-O0_p
  • O1 mencocokkan semua file *.ll-O1 dan *.ll-O1_p
  • O2 mencocokkan semua file *.ll-O2 dan *.ll-O2_p
  • O3 mencocokkan semua file *.ll-O3 dan *.ll-O3_p
  • Og mencocokkan semua file *.ll-Og dan *.ll-Og_p
  • Os mencocokkan semua file *.ll-Os dan *.ll-Os_p
  • Oz mencocokkan semua file *.ll-Oz dan *.ll-Os_z
  • prod mencocokkan semua file *_p
  • any yang cocok dengan semua file
• Opsi -c digunakan untuk menentukan checker yang akan dijalankan, salah satunya:
  • uninit : Pemeriksa memori yang tidak diinisialisasi
  • heapoob : Pemeriksa Malloc OOB
  • concroob : Pemeriksa OOB Indeks Negatif
  • userinput : Pemeriksa Input Pengguna

Contoh

Untuk menemukan bug akses memori yang tidak diinisialisasi yang ditemukan oleh alat kami di Perpustakaan Prio Firefox:

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

Alat ini menandai dua bug. Mari kita lihat yang pertama:

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

Jika Anda memeriksa fungsi serial_read_mp_array (), jalur blok buggy adalah %4 (blok pertama) hingga %71 , di mana kami menggunakan [ %73 ].

Membantu

Kami belum menguji (dan kemungkinan tidak akan menguji) sys pada apa pun kecuali Arch Linux. Kami senang mengintegrasikan tambalan yang menambah dukungan untuk OS lainnya dan membangun sistem!

Struktur Direktori

 ├── 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