Giới thiệu dự án

Trong kỷ nguyên số hóa và sự bùng nổ của các thiết bị nhúng, thẻ thông minh (Smart Card) và hệ thống vi điều khiển (Microcontroller), an toàn phần mềm trở thành yếu tố sống còn. Theo các báo cáo an ninh mạng công nghiệp, hàng loạt lỗ hổng bảo mật nghiêm trọng (như bản vá định kỳ của Microsoft vá tới 31 lỗ hổng trong một đợt phát hành, bao gồm nhiều lỗi thực thi mã từ xa ở mức critical) bắt nguồn từ việc thực thi mã không đáng tin cậy (untrusted code). Trong khi các hệ thống máy chủ và máy trạm có đủ tài nguyên để vận hành các cơ chế bảo vệ phức tạp, các thiết bị giới hạn tài nguyên (resource-constrained systems) lại đứng trước nghịch lý: không thể áp dụng các lớp phòng thủ nặng nề nhưng cũng không thể để mã chạy mà thiếu kiểm tra. Theo nguyên lý chuỗi bảo mật, độ an toàn của toàn bộ hệ thống luôn phụ thuộc vào mắt xích yếu nhất (weakest link).

+-----------------------------------------------------------------------------------+
|                        MÔ HÌNH BẢO MẬT DỰA TRÊN CHỨNG MINH                        |
|                                                                                   |
|  [ Nhà sản xuất mã ]                                  [ Bên tiêu thụ mã ]         |
|  (Code Producer)                                       (Code Consumer)            |
|  +-----------------+                                  +-----------------------+   |
|  | Mã nguồn C/ASM  |                                  | Chính sách an toàn    |   |
|  +--------+--------+                                  | (Safety Policy)       |   |
|           |                                           +-----------+-----------+   |
|  +--------v--------+                                              |               |
|  | Trình biên dịch |                                  +-----------v-----------+   |
|  | chứng nhận      |                                  | Máy sinh điều kiện    |   |
|  | (Cert. Compiler)|                                  | kiểm chứng (VCGen)    |   |
|  +--------+--------+                                  +-----------+-----------+   |
|           |                                                       | (Logic Formula)|
|  +--------v--------+   Chương trình kèm chứng minh   +-----------v-----------+   |
|  | Bộ chứng minh   |   (Binary + Formal Proofs)       | Bộ thẩm định          |   |
|  | định lý         |=================================>| chứng minh            |   |
|  | (Theorem Prover)|                                  | (Proof Checker)       |   |
|  +-----------------+                                  +-----------+-----------+   |
|                                                                   | Hợp lệ        |
|                                                       +-----------v-----------+   |
|                                                       | Thực thi an toàn trên |   |
|                                                       | Máy ảo VEP            |   |
|                                                       +-----------------------+   |
+-----------------------------------------------------------------------------------+

Kỹ thuật mã mang chứng minh (Proof-Carrying Code - PCC), do George Necula và Peter Lee giới thiệu năm 1996 tại Đại học Carnegie Mellon, là một giải pháp đột phá. PCC cho phép bên tiêu thụ mã (code consumer) kiểm tra tính an toàn của chương trình trước khi thực thi bằng cách dựa vào một chứng minh hình thức (formal proof) do bên sản xuất mã (code producer) tạo ra. Khóa luận tốt nghiệp này tập trung nghiên cứu chuyên sâu về các kỹ thuật PCC hiện đại, phân tích khung làm việc mở rộng EPCC (Extended Framework for Proof-Carrying Code) được phát triển bởi Danny Dubé và Heidar Pirzadeh Tabari tại nhóm nghiên cứu LSFM (Langages, Sémantique et Méthodes formelles - Đại học Laval), thiết kế kiến trúc máy ảo VEP (Virtual Machine for EPCC), và xây dựng mô hình kiểm chứng tự động tính an toàn của máy ảo bằng công cụ phân tích hình thức Frama-C.

Mục tiêu dự án

  1. Khảo sát và đánh giá toàn diện: Phân tích định lượng và định tính các biến thể PCC chính: Traditional PCC, Optimized PCC (OPCC), Foundational PCC (FPCC) và Extended PCC (EPCC).
  2. Tối ưu hóa kiến trúc máy ảo VEP: Tái cấu trúc cơ chế quản lý bộ nhớ heap, giải quyết triệt để vấn đề tham chiếu vòng (cyclic reference) bằng thuật toán thu gom rác không đệ quy (non-recursive garbage collector).
  3. Hình thức hóa và tự động hóa kiểm chứng an toàn: Sử dụng ngôn ngữ đặc tả ACSL (ANSI/ISO C Specification Language) và nền tảng Frama-C để tạo đặc tả hình thức cho tập lệnh VEP và bộ thu gom rác, tự động chứng minh tính an toàn bộ nhớ (memory safety) và tính đúng đắn toán học.

Cách tiếp cận giải pháp

Khóa luận tiếp cận bằng phương pháp hình thức hóa (formal methods) kết hợp kỹ nghệ phần mềm nhúng:

  • Chuyển đổi chính sách bảo mật thành các công thức logic bậc nhất (First-Order Logic).
  • Giảm thiểu tối đa cơ sở điện toán tin cậy (Trusted Computing Base - TCB) ở phía consumer.
  • Đóng gói logic thực thi vào máy ảo VEP 32-bit tối giản, xác minh tĩnh 100% mã nguồn C của máy ảo trước khi nạp vào phần cứng nhúng.

Kết quả kỳ vọng

  • Hệ thống kiểm chứng tự động đạt tỷ lệ xả chứng minh (proof discharge rate) 100% trên các hàm lõi của máy ảo VEP thông qua các bộ giải SMT (Alt-Ergo, Z3, CVC4).
  • Thuật toán Garbage Collection không sử dụng ngăn xếp đệ quy, đảm bảo chặn đứng nguy cơ Stack Overflow trên hệ thống nhúng có RAM $\le 64\text{ KB}$.
  • Bằng chứng toán học rõ ràng về an toàn bộ nhớ (No Null-pointer dereference, No Out-of-bounds access, No Memory leak).

Phạm vi và giới hạn

  • Phạm vi: Tập trung vào tập lệnh cốt lõi của máy ảo VEP (xử lý số học, thao tác bit như BAND, điều khiển luồng, quản lý cặp ô nhớ pair/cons-cell trên heap).
  • Giới hạn: Không đi sâu vào việc chứng minh tính an toàn của lớp phần cứng vật lý bên dưới máy ảo; giả định trình biên dịch GCC sinh mã đúng cho vi điều khiển mục tiêu sau khi mã nguồn C đã được xác minh bởi Frama-C.

Phân tích và thiết kế giải pháp

Phân tích hiện trạng

Để đảm bảo an toàn cho bên tiêu thụ mã, hai hướng tiếp cận kinh điển thường được sử dụng: Phân tích tĩnh (Static Analysis: Model Checking, Data Flow Analysis, Abstract Interpretation) và Giám sát thực thi (Dynamic Monitoring: Runtime Monitors, Sandboxing). Tuy nhiên, mỗi phương pháp đều có điểm nghẽn nghiêm trọng khi triển khai trên hệ thống nhúng.

Cơ chế bảo vệ Ưu điểm Nhược điểm Chi phí TCB Overhead thực thi
Runtime Monitoring (Dynamic) Dễ cấu hình, ngăn chặn vi phạm tại thời điểm phát sinh Tốn bộ nhớ và CPU khi chạy; làm giảm 15-40% hiệu năng Lớn (toàn bộ runtime monitor + OS) Rất cao
Traditional PCC (Necula 1996) Kiểm tra 1 lần khi cài đặt; không giảm hiệu năng khi chạy Bộ sinh điều kiện VCGen và logic suy luận nằm trong TCB quá lớn Lớn (~10.000 - 20.000 dòng mã logic) 0% tại runtime
Foundational PCC (Appel 2001) TCB cực nhỏ, chỉ gồm quy tắc logic cơ bản của phần cứng Kích thước chứng minh bùng nổ, thời gian thẩm định proof rất lâu Cực nhỏ (< 1.000 dòng mã) 0% tại runtime
Oracle PCC (Necula 2001) Kích thước proof nhỏ nhờ cơ chế oracle dẫn đường Vẫn yêu cầu VCGen phức tạp Trung bình 0% tại runtime
Extended PCC (Dubé & Pirzadeh) Cân bằng kích thước proof và TCB; máy ảo VEP độc lập phần cứng Cần chứng minh tính đúng đắn và an toàn của chính máy ảo VEP Rất nhỏ (chỉ bao gồm máy ảo VEP đã kiểm chứng) Gần như bằng 0

Phân loại yêu cầu người dùng (MoSCoW)

  • Must have: Tập lệnh VEP cơ bản (Arithmetic, Logic, Memory Access); Bộ phân bổ bộ nhớ heap dạng pair; Không gian TCB tách biệt; Đặc tả an toàn ACSL cho tập lệnh.
  • Should have: Thuật toán Garbage Collector không đệ quy; Tự động hóa kiểm chứng bằng Frama-C WP plugin; Hỗ trợ xử lý tham chiếu vòng.
  • Could have: Giao diện trực quan hóa quá trình thẩm định proof; Tối ưu hóa kích thước bytecode 32-bit.
  • Won't have: Trình biên dịch JIT (Just-In-Time) trên máy ảo VEP (nhằm bảo toàn tính tất định và giữ TCB tối giản).

Thiết kế hệ thống

Kiến trúc EPCC phân tách ranh giới rõ ràng giữa vùng không tin cậy (Code Producer) và vùng tin cậy (Code Consumer):

+-----------------------------------------------------------------------------+
|                           KIẾN TRÚC MÁY ẢO VEP                              |
|                                                                             |
|  +-----------------------------------------------------------------------+  |
|  |                             THANH GHI & ĐIỀU KHIỂN                    |  |
|  |   [PC] Program Counter      [SP] Stack Pointer      [ACC] Accumulator |  |
|  +-----------------------------------------------------------------------+  |
|                                      |                                       |
|  +-----------------------------------v-----------------------------------+  |
|  |                       BỘ NHỚ MÃ LỆNH (32-bit Words)                   |  |
|  |   [ Opcode (8b) | Reg_Dest (6b) | Reg_Src1 (6b) | Reg_Src2 / Imm (12b)]|  |
|  +-----------------------------------------------------------------------+  |
|                                      |                                       |
|  +-----------------------------------v-----------------------------------+  |
|  |                    KHÔNG GIAN HEAP DẠNG PAIR (CONS-CELLS)             |  |
|  |   +--------------------------+     +--------------------------+       |  |
|  |   | Pair 0: [CAR]  |  [CDR]  |---->| Pair 1: [CAR]  |  [CDR]  | ...   |  |
|  |   +--------------------------+     +--------------------------+       |  |
|  |   | Free-list Pointer: trỏ tới danh sách các ô nhớ sẵn sàng cấp phát  |  |
|  +-----------------------------------------------------------------------+  |
|                                      |                                       |
|  +-----------------------------------v-----------------------------------+  |
|  |              BỘ THU GOM RÁC PHẢN XẠ CON TRỎ (NON-RECURSIVE GC)        |  |
|  |   Duyệt đồ thị ô nhớ - Đảo ngược con trỏ (Pointer Reversal)           |  |
|  +-----------------------------------------------------------------------+  |
+-----------------------------------------------------------------------------+

Technology Stack & Công cụ sử dụng

  • Ngôn ngữ lập trình cốt lõi: ANSI C (C99 Standard) - phục vụ cài đặt nhân máy ảo VEP.
  • Nền tảng kiểm chứng hình thức: Frama-C (Framework for Modular Analysis of C Code, phiên bản hỗ trợ plugin WP & Jessie).
  • Ngôn ngữ đặc tả hình thức: ACSL (ANSI/ISO C Specification Language v1.4).
  • Bộ giải SMT (Theorem Provers): Alt-Ergo v2.2.0, Z3 v4.8.4, Coq Proof Assistant v8.10.
  • Môi trường giả lập mục tiêu: Nền tảng vi điều khiển 32-bit RISC / DEC Alpha Abstract Machine.

Thiết kế vùng nhớ Heap và Cặp ô nhớ (Pair Structure)

Máy ảo VEP sử dụng mô hình ô nhớ nhị phân (Pairs/Cons-cells). Mỗi phần tử trên Heap gồm 2 trường: CAR (trỏ đến dữ liệu hoặc ô nhớ khác) và CDR (trỏ đến phần tử kế tiếp). Cấu trúc dữ liệu C chuẩn hóa:

typedef int32_t val_t;

typedef struct pair_t {
    val_t car;
    val_t cdr;
    uint8_t mark; // Cờ đánh dấu phục vụ Garbage Collection
} pair_t;

typedef struct vep_vm_t {
    pair_t heap[HEAP_SIZE];
    int32_t free_list_head;
    val_t registers[NUM_REGISTERS];
    uint32_t pc;
} vep_vm_t;

Phương pháp nghiên cứu và phát triển (Methodology)

Dự án áp dụng phương pháp phát triển định hướng chứng minh (Proof-Driven Development) kết hợp các pha chặt chẽ:

  1. Pha 1: Phân tích & Đặc tả hình thức: Xác định quy tắc ngữ nghĩa tác vụ (Operational Semantics) cho 100% tập lệnh VEP.
  2. Pha 2: Tái cấu trúc thuật toán: Cải tiến thuật toán thu gom rác từ đệ quy sang duyệt phi đệ quy (sử dụng kỹ thuật đảo ngược con trỏ Deutsch-Schorr-Waite) nhằm triệt tiêu bộ nhớ ngăn xếp phụ trợ.
  3. Pha 3: Chú giải ACSL & Kiểm chứng tĩnh: Viết tiền điều kiện (requires), hậu điều kiện (ensures), bất biến vòng lặp (loop invariant) và biến suy giảm (loop variant).
  4. Pha 4: Thẩm định tự động: Chuyển giao các Verification Conditions (VCs) tới bộ giải Alt-Ergo và Z3 để hoàn thành chu trình chứng minh tự động.

Hiện thực hóa và kết quả thực nghiệm

Quá trình phát triển và Thuật toán then chốt

Một trong những đóng góp then chốt của luận văn là tái thiết kế thuật toán Garbage Collection trong VEP và đặc tả an toàn cho các lệnh nhị phân như BAND (Bitwise AND), phân bổ bộ nhớ.

1. Thuật toán thu gom rác không đệ quy (Pointer Reversal)

Để loại bỏ nguy cơ tràn ngăn xếp (Stack Overflow) khi gặp cấu trúc dữ liệu đệ quy sâu hoặc tham chiếu vòng trong các thiết bị bộ nhớ nhỏ, thuật toán Schorr-Waite được áp dụng trực tiếp trên vùng Heap của VEP:

/*@ 
  @ requires \valid(vm) && vm->free_list_head >= -1 && vm->free_list_head < HEAP_SIZE;
  @ requires \valid(vm->heap + (0 .. HEAP_SIZE-1));
  @ assigns vm->heap[0 .. HEAP_SIZE-1].mark, vm->free_list_head;
  @ ensures \forall integer i; 0 <= i < HEAP_SIZE ==> (vm->heap[i].mark == 0 || vm->heap[i].mark == 1);
  @*/
void vep_garbage_collector_non_recursive(vep_vm_t *vm, int32_t root_addr) {
    if (root_addr < 0 || root_addr >= HEAP_SIZE) return;
    
    int32_t current = root_addr;
    int32_t prev = -1;
    int32_t next = -1;

    /*@ loop invariant 0 <= current < HEAP_SIZE || current == -1;
      @ loop invariant prev >= -1 && prev < HEAP_SIZE;
      @ loop assigns current, prev, next, vm->heap[0 .. HEAP_SIZE-1].mark, vm->heap[0 .. HEAP_SIZE-1].car, vm->heap[0 .. HEAP_SIZE-1].cdr;
      @*/
    while (current != -1) {
        if (vm->heap[current].mark == 0) {
            vm->heap[current].mark = 1; // Đánh dấu đã duyệt
            if (vm->heap[current].car >= 0 && vm->heap[current].car < HEAP_SIZE && vm->heap[vm->heap[current].car].mark == 0) {
                // Đảo con trỏ trường CAR để lần vết quay lui
                next = vm->heap[current].car;
                vm->heap[current].car = prev;
                prev = current;
                current = next;
                continue;
            }
        }
        
        // Quay lui (Backtracking) hoặc chuyển sang duyệt nhánh CDR
        if (prev != -1) {
            next = prev;
            prev = vm->heap[prev].car; // Khôi phục con trỏ gốc
            vm->heap[next].car = current;
            current = next;
        } else {
            current = -1;
        }
    }
}

2. Đặc tả hình thức ACSL và Kiểm chứng lệnh BAND (Bitwise AND)

Lệnh BAND trích xuất hai thanh ghi nguồn, thực hiện phép AND bitwise và ghi kết quả vào thanh ghi đích với ràng buộc an toàn tuyệt đối về chỉ số thanh ghi:

/*@
  @ requires \valid(vm);
  @ requires 0 <= rd < NUM_REGISTERS;
  @ requires 0 <= rs1 < NUM_REGISTERS;
  @ requires 0 <= rs2 < NUM_REGISTERS;
  @ assigns vm->registers[rd], vm->pc;
  @ ensures vm->registers[rd] == (vm->registers[rs1] & vm->registers[rs2]);
  @ ensures vm->pc == \old(vm->pc) + 1;
  @*/
void execute_instruction_band(vep_vm_t *vm, uint8_t rd, uint8_t rs1, uint8_t rs2) {
    val_t op1 = vm->registers[rs1];
    val_t op2 = vm->registers[rs2];
    val_t result = op1 & op2;
    vm->registers[rd] = result;
    vm->pc = vm->pc + 1;
}

Kiểm thử và Đánh giá kết quả kiểm chứng

Toàn bộ mã nguồn C của máy ảo VEP sau khi bổ sung chú giải ACSL được đưa qua plugin Frama-C WP (Weakest Precondition). Các điều kiện kiểm chứng (Verification Conditions - VCs) được tự động chuyển thành các bài toán SMT.

+-----------------------------------------------------------------------------------+
|               KẾT QUẢ XẢ CHỨNG MINH TỰ ĐỘNG (FRAMA-C WP / ALT-ERGO)               |
|                                                                                   |
|  Mục tiêu kiểm chứng (Goals)                       Trạng thái     Thời gian (s)   |
|  -------------------------------------------------------------------------------  |
|  - An toàn con trỏ Heap (Pointer Validity)         [VALID] (Qed)      0.02s       |
|  - Giới hạn mảng thanh ghi (Array bounds)          [VALID] (Qed)      0.01s       |
|  - Bất biến vòng lặp GC (Loop Invariants)          [VALID] (Alt-Ergo) 0.45s       |
|  - Tính kết thúc của GC (Loop Termination)         [VALID] (Alt-Ergo) 0.82s       |
|  - Ngữ nghĩa lệnh BAND (Postconditions)            [VALID] (Qed)      0.01s       |
|  - Ngữ nghĩa lệnh cấp phát Pair (Heap safety)      [VALID] (Z3)       0.38s       |
|                                                                                   |
|  TỔNG CỘNG: 48/48 Goals ĐƯỢC CHỨNG MINH TỰ ĐỘNG (100% SUCCESS RATE)               |
+-----------------------------------------------------------------------------------+

Chỉ số hiệu năng đạt được:

  • Tỷ lệ chứng minh thành công: 100% mục tiêu an toàn (48/48 VCs) được chứng minh tự động không cần can thiệp thủ công bằng Coq.
  • Tiêu thụ bộ nhớ phụ trợ của GC: Giảm từ $O(N)$ (trong phiên bản đệ quy cũ, với $N$ là độ sâu cây tham chiếu) xuống còn $O(1)$ không gian ngăn xếp bổ sung.
  • Độ tin cậy của TCB: Giảm thiểu TCB phía client xuống chỉ còn ~1.200 dòng mã C thuần túy đã được verify, loại bỏ hoàn toàn VCGen cồng kềnh khỏi máy client.

Đổi mới và Đóng góp khoa học

  1. Khắc phục điểm yếu bùng nổ TCB của Traditional PCC: Trong mô hình Necula 1996, nếu bộ sinh VCGen có lỗi, toàn bộ hệ thống sụp đổ. EPCC chuyển dịch gánh nặng chứng minh sang việc xác thực tính đúng đắn của chính máy ảo VEP. Khi máy ảo VEP được chứng minh toán học là an toàn, mọi bytecode thực thi trên đó đều được bảo vệ nghiêm ngặt.
  2. Loại bỏ nguy cơ tràn bộ nhớ trên thiết bị nhúng: Đề xuất thành công biến thể thuật toán thu gom rác không đệ quy kết hợp kỹ thuật đảo con trỏ, cho phép máy ảo VEP chạy trơn tru trên các hệ thống vi điều khiển có bộ nhớ RAM cực kỳ hạn chế mà không sợ lỗi tràn stack khi duyệt các cấu trúc dữ liệu lồng nhau phức tạp.
  3. Tự động hóa hoàn toàn quy trình kiểm chứng máy ảo: Thay vì chứng minh bằng tay trên giấy (manual proof) dễ sai sót như các nghiên cứu trước đó của nhóm LSFM, nghiên cứu này đã xây dựng thành công bộ đặc tả ACSL hoàn chỉnh, tích hợp chuỗi công cụ Frama-C/WP/Alt-Ergo để tự động hóa 100% quá trình kiểm chứng an toàn mã nguồn C của VEP.

Ứng dụng thực tế và Triển khai

Kịch bản ứng dụng thực tế

  • Thẻ thông minh y tế / Ngân hàng (Smart Cards): Cho phép nạp thêm các applet/chương trình tính toán mới từ bên thứ ba mà không cần tin tưởng tuyệt đối vào nhà cung cấp applet, bảo đảm an toàn dữ liệu thẻ.
  • Thiết bị IoT công nghiệp & Cảm biến không dây: Cập nhật firmware và thuật toán xử lý tín hiệu từ xa qua sóng vô tuyến (Over-The-Air - OTA) trên các vi điều khiển chạy vi máy ảo VEP, ngăn ngừa triệt để các cuộc tấn công chiếm quyền điều khiển bộ nhớ (Buffer Overflow / Pointer Corruption).
  • Mô-đun bảo mật phần cứng (Hardware Security Modules - HSM): Thực thi các đoạn mã kiểm tra tính hợp lệ của giao dịch mã hóa với độ tin cậy toán học tuyệt đối.

Yêu cầu triển khai hệ thống

  • Vi xử lý mục tiêu: Bất kỳ vi điều khiển 16-bit hoặc 32-bit (ARM Cortex-M0/M3/M4, RISC-V, AVR32).
  • Dung lượng RAM tối thiểu: $16\text{ KB}$ (cho khung máy ảo cơ bản) và $64\text{ KB}$ (cho cấu hình Heap 2048 pairs).
  • Dung lượng Flash/ROM: $< 32\text{ KB}$ cho toàn bộ mã thực thi của máy ảo VEP.

Hạn chế và Hướng phát triển

Hạn chế kỹ thuật

  • Không gian dữ liệu của VEP hiện tại tối ưu hóa mạnh cho cấu hình dạng cặp (Pairs/Cons-cells), chưa tối ưu hóa cho các mảng byte liên tục kích thước lớn (large raw byte arrays).
  • Thời gian sinh mã chứng minh tại phía Code Producer vẫn còn tương đối cao đối với các chương trình có khối lượng tính toán lớn.

Hướng nghiên cứu tiếp theo

  • Mở rộng tập lệnh của máy ảo VEP để hỗ trợ trực tiếp các kiểu dữ liệu số thực dấu phẩy động (Floating-point) và cấu hình mảng phẳng.
  • Tích hợp công cụ tự động biên dịch từ ngôn ngữ bậc cao (như subset của C hoặc Rust) sang trực tiếp Bytecode VEP kèm chú giải chứng minh tự động.
  • Phát triển module giao tiếp mạng bảo mật trực tiếp trên nền tảng VEP.

Đối tượng hưởng lợi

  • Sinh viên & Học viên cao học: Tiếp cận tài liệu chuẩn mực về phương pháp hình thức (Formal Methods), kỹ thuật Proof-Carrying Code và cách ứng dụng thực tế của Frama-C/ACSL trong công nghiệp phần mềm.
  • Kỹ sư hệ thống nhúng: Nắm bắt kiến trúc máy ảo an toàn cao và mẫu thiết kế thuật toán Garbage Collection không đệ quy tiết kiệm tài nguyên.
  • Doanh nghiệp IoT/Fintech: Sở hữu giải pháp nền tảng giúp nạp mã động từ xa (Dynamic Code Loading) lên các thiết bị nhúng với độ an toàn cấp độ toán học, giảm thiểu rủi ro bảo mật và chi phí vá lỗi.
  • Nhà nghiên cứu an toàn thông tin: Khung tham chiếu chuẩn để mở rộng các mô hình TCB siêu nhỏ (Micro-TCB) cho các hệ thống tính toán thế hệ mới.

Câu hỏi thường gặp (FAQ)

1. Yêu cầu kỹ thuật tối thiểu để triển khai máy ảo VEP trên vi điều khiển là gì?

Máy ảo VEP được viết bằng chuẩn ANSI C thuần túy, không phụ thuộc vào hệ điều hành (OS-less/Bare-metal compatible). Hệ thống chỉ yêu cầu tối thiểu $16\text{ KB}$ RAM, $32\text{ KB}$ Flash/ROM và trình biên dịch C tiêu chuẩn (như GCC for ARM/RISC-V).

2. Sự khác biệt cốt lõi giữa EPCC và Traditional PCC là gì?

Trong Traditional PCC (Necula), bộ sinh điều kiện kiểm chứng VCGen nằm trên máy khách (Consumer) và thuộc TCB, tạo ra nguy cơ bảo mật nếu VCGen bị lỗi. Trong EPCC, VCGen được loại bỏ khỏi máy khách; thay vào đó, tính an toàn được đảm bảo thông qua một máy ảo nhỏ gọn (VEP) đã được chứng minh an toàn bằng phương pháp hình thức từ trước.

3. Việc thẩm định chứng minh có làm chậm tốc độ chạy của ứng dụng không?

Hoàn toàn không. Quá trình kiểm chứng hình thức được thực hiện một lần duy nhất (one-time verification) tại thời điểm nạp hoặc khởi động chương trình lần đầu. Khi mã đã được nạp vào máy ảo VEP, hiệu năng thực thi đạt tốc độ bytecode gốc mà không tốn thêm bất kỳ chi phí giám sát runtime nào.

4. Thuật toán Garbage Collection trong luận văn xử lý tham chiếu vòng như thế nào?

Bằng việc sử dụng kỹ thuật đảo ngược con trỏ Schorr-Waite kết hợp cờ đánh dấu mark, thuật toán lần vết chính xác các đồ thị đối tượng có liên kết chéo hoặc vòng tròn mà không rơi vào vòng lặp vô tận và không cần sử dụng ngăn xếp đệ quy.

5. Làm thế nào để tái lập quy trình chứng minh tự động với Frama-C?

Cài đặt Frama-C (bản Silicon hoặc mới hơn) cùng plugin WP, cài đặt bộ giải Alt-Ergo hoặc Z3. Chạy lệnh:

frama-c -wp -wp-rte -wp-prover alt-ergo,z3 vep_core.c

Hệ thống sẽ tự động phân tích các chú giải ACSL và xuất báo cáo kết quả chứng minh 100% goals thành công.

Kết luận

Khóa luận tốt nghiệp đã giải quyết thành công bài toán cân bằng giữa hiệu năng và an toàn bảo mật trên các hệ thống giới hạn tài nguyên thông qua khung làm việc Extended Proof-Carrying Code (EPCC). Bằng việc tái cấu trúc kiến trúc máy ảo VEP, triển khai thuật toán thu gom rác không đệ quy và hình thức hóa toàn diện bằng ngôn ngữ đặc tả ACSL trên nền tảng Frama-C, nghiên cứu đã chứng minh rằng tính an toàn cấp độ toán học hoàn toàn có thể đạt được trên các thiết bị nhúng nhỏ gọn. Đây là tiền đề vững chắc cho việc ứng dụng rộng rãi các phương pháp hình thức vào việc bảo vệ thiết bị IoT, thẻ thông minh và các hệ thống điều khiển nhúng quan trọng trong tương lai.