Bagikan melalui

Alat Verifikasi Statis dan Dinamis

  • Artikel

Ada dua jenis alat verifikasi dasar:

  • Alat verifikasi statis memeriksa kode driver tanpa menjalankan driver. Karena alat-alat ini tidak bergantung pada pengujian yang menjalankan kode, mereka bisa sangat menyeluruh. Secara teoritis, alat verifikasi statis dapat memeriksa semua kode driver, termasuk jalur kode yang jarang dijalankan dalam praktiknya. Namun, karena driver tidak benar-benar berjalan, mereka dapat menghasilkan hasil positif palsu. Artinya, mereka mungkin melaporkan kesalahan dalam jalur kode yang mungkin tidak terjadi dalam praktiknya.

  • Alat verifikasi dinamis memeriksa kode driver saat driver berjalan, biasanya dengan mencegat panggilan ke rutinitas dukungan driver yang umum digunakan dan mengganti panggilan ke versi pemeriksaan kesalahan mereka sendiri dari rutinitas yang sama. Karena driver benar-benar berjalan saat alat dinamis melakukan verifikasi, hasil positif palsu jarang terjadi. Namun, karena alat dinamis hanya mendeteksi tindakan yang terjadi saat mereka memantau driver, alat dapat melewatkan cacat driver tertentu jika cakupan pengujian driver tidak memadai. Pada saat yang sama, dengan menggunakan informasi yang tersedia pada waktu proses, misalnya, informasi yang lebih sulit diekstrak secara statis dari kode sumber, alat verifikasi dinamis dapat mendeteksi kelas kesalahan driver tertentu yang lebih sulit dideteksi dengan alat analisis statis.

Praktik terbaiknya adalah menggunakan kombinasi alat verifikasi statis dan dinamis. Alat statis memungkinkan Anda memeriksa jalur kode yang sulit dilatih dalam praktiknya, sementara alat dinamis menemukan kesalahan serius yang terjadi di driver.

Penting

Program Kompatibilitas Perangkat Keras Windows memerlukan CodeQL untuk Pengujian Logo Alat Statis (STL) pada Sistem Operasi Klien dan Server kami. Kami akan terus mempertahankan dukungan untuk SDV dan CA pada produk yang lebih lama. Mitra sangat didorong untuk meninjau persyaratan CodeQL untuk Uji Logo Alat Statis. Untuk informasi selengkapnya tentang menggunakan CodeQL, lihat CodeQL dan Uji Logo Alat Statis.

Survei Alat Verifikasi

Alat verifikasi berikut dijelaskan dalam WDK dan direkomendasikan untuk digunakan oleh pengembang driver dan penguji. Mereka tercantum dalam urutan di mana mereka biasanya digunakan.

Segera setelah kode dikompilasi

  • CodeQL, oleh GitHub, adalah mesin analisis kode semantik yang kuat, dan kombinasi serangkaian kueri keamanan bernilai tinggi yang luas bersama dengan platform yang kuat menjadikannya alat yang sangat berharga untuk mengamankan kode driver. Untuk informasi selengkapnya, lihat CodeQL dan Uji Logo Alat Statis.

Alat statis tambahan

Bergantung pada versi Windows tempat Anda membangun driver, alat statis lainnya mungkin diperlukan.

  • Analisis Kode untuk Driver adalah alat verifikasi statis yang berjalan pada waktu kompilasi. Analisis Kode untuk Driver dapat memverifikasi driver yang ditulis dalam C/C++ dan kode terkelola. Ini memeriksa kode di setiap fungsi driver secara independen, sehingga Anda dapat menjalankannya segera setelah Anda dapat membangun driver Anda. Ini berjalan relatif cepat dan menggunakan beberapa sumber daya.

    Fitur dasar alat Analisis Kode di Visual Studio mendeteksi kesalahan pengodean umum, seperti tidak memeriksa nilai yang dikembalikan. Fitur khusus driver mendeteksi kesalahan pengodean driver yang lebih halus, seperti meninggalkan bidang yang tidak diinisialisasi dalam IRP yang disalin dan gagal memulihkan IRQL yang diubah pada akhir rutinitas.

  • Static Driver Verifier (SDV) adalah alat verifikasi statis yang berjalan pada waktu kompilasi dan memverifikasi kode driver mode kernel yang ditulis dalam C/C++. Ini termasuk dalam WDK dan dapat dimulai dari Visual Studio Ultimate 2012 atau dari jendela prompt Perintah Visual Studio menggunakan MSBuild.

    Berdasarkan serangkaian aturan antarmuka dan model sistem operasi, Verifier Driver Statis menentukan apakah driver berinteraksi dengan benar dengan kernel sistem operasi Windows. Verifier Driver Statis sangat menyeluruh -- ia menjelajahi semua jalur yang dapat dijangkau dalam kode sumber driver dan mengeksekusinya secara simbolis. Dengan demikian, ia menemukan bug yang tidak terdeteksi dengan menggunakan metode pengujian driver konvensional lainnya.

Penting

SDV tidak lagi didukung dan SDV tidak tersedia di rilis Windows 24H2 WDK atau EWDK. Ini tidak tersedia di WDK yang lebih baru dari build 26017, dan tidak termasuk dalam WDK Windows 24H2 RTM. SDV masih dapat digunakan dengan mengunduh Windows 11, versi 22H2 EWDK (dirilis 24 Oktober 2023) dengan alat build Visual Studio 17.1.5 dari Unduh Windows Driver Kit (WDK). Hanya penggunaan Enterprise WDK untuk menjalankan SDV yang direkomendasikan. Menggunakan versi WDK standar yang lebih lama bersama dengan rilis Terbaru Visual Studio tidak disarankan, karena ini kemungkinan akan mengakibatkan kegagalan analisis.
Ke depannya, CodeQL akan menjadi alat analisis statis utama untuk driver. CodeQL menyediakan bahasa kueri canggih yang memperlakukan kode sebagai database yang akan dikueri, sehingga mudah untuk menulis kueri untuk perilaku, pola, dan lainnya tertentu. Untuk informasi selengkapnya tentang menggunakan CodeQL, lihat CodeQL dan Uji Logo Alat Statis.

Ketika driver berjalan

Gunakan alat verifikasi dinamis berikut segera setelah driver dibangun dan berjalan tanpa kesalahan yang jelas.

  • Driver Verifier adalah alat verifikasi dinamis yang ditulis terutama untuk driver Windows. Ini termasuk beberapa pengujian yang dapat dijalankan pada beberapa driver secara bersamaan. Driver Verifier sangat efektif dalam menemukan bug serius pada driver yang berpengalaman pengembang driver dan penguji mengonfigurasi Driver Verifier untuk berjalan setiap kali driver mereka berjalan di lingkungan pengembangan atau pengujian. Pemverifikasi Driver disertakan dalam Windows. Saat mengaktifkan Driver Verifier untuk driver, Anda juga harus menjalankan beberapa pengujian pada driver. Driver Verifier dapat mendeteksi bug driver tertentu yang sulit dideteksi dengan menggunakan alat verifikasi statis saja. Contoh jenis bug ini meliputi yang berikut ini:

    • Buffer kumpulan kernel overruns. Ketika driver terverifikasi mengalokasikan buffer memori kumpulan, Driver Verifier melindunginya dengan halaman memori yang tidak dapat diakses. Jika driver mencoba menggunakan memori melewati akhir buffer, Driver Verifier akan mengeluarkan pemeriksaan bug.

    • Menggunakan memori setelah membebaskannya. Blok memori kumpulan khusus menggunakan halaman memori mereka sendiri, dan jangan berbagi halaman memori dengan alokasi lain. Ketika driver membebaskan blok memori kumpulan, halaman memori yang sesuai menjadi tidak dapat diakses. Jika driver mencoba menggunakan memori tersebut setelah membebaskannya, driver akan langsung mengalami crash.

    • Menggunakan memori yang dapat di-pageable saat berjalan pada IRQL yang ditinggikan. Ketika driver terverifikasi menaikkan IRQL pada DISPATCH_LEVEL atau lebih tinggi, Driver Verifier memangkas semua memori yang dapat di-pageable dari set kerja sistem, mensimulasikan sistem di bawah tekanan memori. Driver mengalami crash jika mencoba menggunakan salah satu alamat virtual yang dapat di-pageable ini.

    • Simulasi Sumber Daya Rendah. Untuk mensimulasikan sistem dalam kondisi sumber daya rendah, Driver Verifier dapat gagal berbagai API kernel sistem operasi yang dipanggil oleh driver.

    • Kebocoran memori. Driver Verifier melacak alokasi memori yang dibuat oleh driver dan memastikan memori dibebaskan sebelum driver dibongkar.

    • Operasi I/O yang membutuhkan terlalu banyak waktu untuk diselesaikan atau dibatalkan. Driver Verifier dapat menguji logika driver untuk merespons STATUS_PENDING mengembalikan nilai dari IoCallDriver.

    • Pemeriksaan Kepatuhan DDI. (Tersedia dimulai dengan Windows 8) Driver Verifier menerapkan serangkaian aturan antarmuka driver perangkat (DDI) yang memeriksa interaksi yang tepat antara driver dan antarmuka kernel sistem operasi. Aturan ini sesuai dengan aturan yang digunakan Pemverifikasi Driver Statis dalam menganalisis kode sumber driver. Jika Pemverifikasi Driver menemukan kesalahan saat Pemeriksaan Kepatuhan DDI diaktifkan, jalankan Pemverifikasi Driver Statis dan pilih aturan yang sama yang menyebabkan kesalahan. Verifier Driver Statis dapat membantu Anda menemukan penyebab cacat dalam kode sumber driver.

  • Application Verifier adalah alat verifikasi dinamis untuk aplikasi mode pengguna dan driver yang ditulis dalam C/C++. Ini tidak memverifikasi kode terkelola.