Trần Ngọc Minh

Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly

Tài liệu trình bày về Owi, một bộ công cụ kiểm tra và thực thi biểu tượng (symbolic execution) dành cho WebAssembly (Wasm), được phát triển bằng ngôn ngữ lập trình OCaml. Owi có khả năng thực hiện kiểm tra lỗi trên mã nguồn C, Rust và các ngôn ngữ biên dịch sang Wasm, đồng thời hỗ trợ thực thi song song để cải thiện hiệu suất.

1. Giới Thiệu (Introduction)

  • WebAssembly (Wasm) là một định dạng nhị phân hiệu suất cao, ban đầu được phát triển cho các ứng dụng web, nhưng hiện nay đã được mở rộng sang máy chủ, IoT, blockchain, và các hệ thống nhúng.
  • Dù có các cơ chế bảo mật, Wasm vẫn dễ bị buffer overflow, memory leak, và các lỗ hổng bảo mật khác.
  • Symbolic Execution là một kỹ thuật giúp phân tích tất cả các đường đi có thể của chương trình, bằng cách thay thế giá trị đầu vào bằng các biến tượng trưng.
  • Owi là một công cụ thực thi biểu tượng đa luồng, hiệu suất cao, có khả năng kiểm tra mã Wasm được biên dịch từ C và Rust.

Các đóng góp chính của Owi:

  1. Owi Toolkit: Một bộ công cụ kiểm tra mã Wasm trong hệ sinh thái OCaml.
  2. Symbolic Execution mở rộng: Hỗ trợ thực thi biểu tượng song song.
  3. Kiểm tra lỗi đa ngôn ngữ: Có thể phát hiện lỗi trong mã nguồn C, Rust, và chương trình hỗn hợp.

2. Kiến Thức Nền Tảng (Background)

2.1 WebAssembly (Wasm)

  • Wasm là một mô hình máy ảo stack-based (stack machine), chạy các chương trình biên dịch từ C, C++, Rust, Go, OCaml, Java, v.v.
  • Một chương trình Wasm bao gồm:
    • Module: Chứa các hàm, biến toàn cục và bộ nhớ tuyến tính.
    • Stack: Điều hành các thao tác toán học và logic.
    • Linear Memory: Bộ nhớ tuyến tính được chia sẻ giữa các module.
  • Wasm hỗ trợ 4 kiểu dữ liệu chính: i32, i64, f32, f64.

Ví dụ mã Wasm:

(module
  (func $test_swap (param $x i32) (param $y i32)
    (if (i32.gt_s (local.get $x) (local.get $y))
      (then
        (local.set $x (i32.add (local.get $x) (local.get $y)))
        (local.set $y (i32.sub (local.get $x) (local.get $y)))
        (local.set $x (i32.sub (local.get $x) (local.get $y)))
      )
    )
  )
)

Chức năng: Hoán đổi giá trị x và y nếu x > y.

2.2 Symbolic Execution

  • Nguyên lý: Thay vì chạy với giá trị cụ thể, chương trình chạy với các biến tượng trưng, cho phép kiểm tra mọi trường hợp có thể xảy ra.
  • Mô hình toán học:
    • Biểu diễn mỗi nhánh điều kiện dưới dạng ràng buộc đại số.
    • Sử dụng trình giải SMT (Satisfiability Modulo Theories) để tìm lỗi.
  • Ứng dụng: Phát hiện lỗi integer overflow, buffer overflow, memory leaks.

3. Chuyển Đổi Trình Thông Dịch Thành Phiên Bản Dựa Trên Monad

Ý tưởng chính: Viết trình thông dịch dựa trên mô hình Monad, giúp linh hoạt hóa việc thực thi mã.

3.1 Trình thông dịch cơ bản

  • Viết bằng OCaml, hỗ trợ thực thi mã Wasm.
type value = I32 of int32 | I64 of int64
let eval_instr i stack =
  match i, stack with
  | Binop Add, I32 x :: I32 y :: stack -> I32 (Int32.add x y) :: stack
  | Binop Gt, I32 x :: I32 y :: stack -> I32 (if x > y then 1l else 0l) :: stack
  | _ -> failwith "Unhandled instruction"

3.2 Trình thông dịch tham số hóa

  • Trừu tượng hóa kiểu dữ liệu, giúp dễ dàng mở rộng.
module type Value_intf = sig
  module Int32 : sig
    type t
    val add : t -> t -> t
  end
end

3.3 Trình thông dịch dựa trên Monad

  • Thêm Monad để hỗ trợ symbolic execution.
module type Choice_intf = sig
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
end

Lợi ích:

  • Hỗ trợ song song hóa.
  • Hỗ trợ symbolic execution.

4. Monad Lựa Chọn (Choice Monad)

  • Xử lý đa luồng, chia nhánh, và quản lý bộ nhớ trong symbolic execution.
  • Hỗ trợ forking, yielding, và lazy memory.

4.1 Triển khai Monad song song

  • Sử dụng OCaml multicore scheduler để chạy song song.
let rec bind (mx : ('a, 'wls) t) (f : 'a -> ('b, 'wls) t) : ('b, 'wls) t =
  Schedulable (fun wls -> unfold_status (run mx wls))

4.2 Mô hình bộ nhớ lười (Lazy Memory Model)

  • Copy-on-write: Chỉ sao chép bộ nhớ khi cần.
  • Giảm tiêu thụ RAM khi thực hiện symbolic execution.

5. Khả Năng Kiểm Tra Lỗi

5.1 Wasm

  • Kiểm tra lỗi buffer overflow, integer overflow.
$ owi sym test_swap.wat
Trap: unreachable
Model:
(symbol_0 (i32 2147483646))
(symbol_1 (i32 -2147483647))

5.2 C và Rust

  • Kiểm tra lỗi biên dịch C sang Wasm.
  • So sánh tính tương đương của hàm giữa C và Rust.
#include <owi.h>
void main(void) {
  int x = owi_i32();
  float y = owi_f32();
  owi_assert(f(x, y) == 42);
}
  • Kiểm tra lỗi trong thư viện Rust gọi C.

6. Đánh Giá Thực Nghiệm

  • Nhanh hơn 313× so với Manticore, 57× so với SeeWasm.
  • Phát hiện 676 lỗi trong 30 giây trên tập dữ liệu Test-Comp 2024.
  • Không có false negatives, trong khi KLEE và Symbiotic có 7.67% và 12.37%.

7. Kết Luận

  • Owi là công cụ symbolic execution mạnh mẽ, hỗ trợ đa luồng.
  • Hữu ích cho kiểm thử C, Rust, và Wasm.
  • Tương lai: Hỗ trợ WasmerGC, kiểm tra Java/Scala, cải tiến thuật toán heuristic.
Posted in , ,