Tổng quan luận án

Tính cấp thiết và khoảng trống nghiên cứu

Trong lĩnh vực an toàn thông tin, phân tích pháp chứng máy tính (computer forensic analysis) là quá trình tìm hiểu, tái tạo và phân tích các sự kiện tùy ý đã diễn ra trong quá khứ nhằm xác định nguyên nhân, diễn biến và hệ quả của các sự cố an ninh. Theo luận án của Sean Philip Peisert (2007) tại Đại học California, San Diego (UCSD), thực trạng điều tra pháp chứng máy tính phần lớn mang tính tùy tiện (ad hoc), dựa nhiều vào may mắn hoặc năng lực cá nhân của một số ít chuyên gia thay vì một phương pháp luận khoa học có tính hệ thống.

Vấn đề cốt lõi mà tác giả chỉ ra xuất phát từ sự tách rời hoàn toàn giữa hai khâu: ghi vết (logging) và kiểm toán/phân tích (auditing). Quản trị viên hệ thống thiết lập dữ liệu ghi nhật ký độc lập với mục tiêu của chuyên gia phân tích pháp chứng. Dữ liệu nhật ký hiện hành thường được thu thập phục vụ mục đích gỡ lỗi phần mềm (như syslog trong UNIX) hoặc dựa trên các phán đoán chủ quan về những gì được cho là quan trọng (như Sun Basic Security Module - BSM).

Hệ quả là các hệ thống ghi nhận quá nhiều dữ liệu không phù hợp—dữ liệu dư thừa, dữ liệu rác không liên quan hoặc dữ liệu bị kẻ tấn công cố tình tạo ra để đánh lạc hướng—trong khi lại thiếu hụt dữ liệu trọng yếu. Thực tiễn này buộc các nhà phân tích phải đánh đổi giữa khối lượng dữ liệu khổng lồ gây quá tải tài nguyên và dung lượng lưu trữ, hoặc lượng dữ liệu quá ít khiến kết luận điều tra phải dựa trên suy đoán (inference) thay vì suy luận logic mang tính diễn dịch (deduction). Khoảng trống nghiên cứu được xác định là sự thiếu vắng một mô hình hình thức có khả năng xác định chính xác những dữ liệu tối thiểu và cần thiết phải ghi nhận để phục vụ việc tái dựng sự kiện một cách chính xác.

Mục tiêu và nhiệm vụ nghiên cứu

Mục tiêu tổng quát của luận án là xây dựng một mô hình hình thức và phương pháp luận ghi nhật ký định hướng mục tiêu (goal-oriented logging) nhằm tối ưu hóa dữ liệu cần thu thập, bảo toàn khả năng tái dựng và phân tích các cuộc tấn công mà không làm quá tải hệ thống hay gây cản trở cho người phân tích.

Các câu hỏi và nhiệm vụ nghiên cứu được văn bản xác định cụ thể như sau:

  1. Xác định cuộc xâm nhập đã diễn ra như thế nào (how an intrusion occurred).
  2. Xác định kẻ tấn công đã thực hiện những hành vi cụ thể nào trong suốt quá trình xâm nhập (what the attacker did during the intrusion).
  3. Xác định các tác động và hệ quả do hành động của kẻ tấn công gây ra đối với hệ thống (what the effects of the attack were).
  4. Xác định mối liên hệ giữa các hành vi chuyển trạng thái hệ thống với người dùng hoặc tiến trình chịu trách nhiệm thực thi (associating users with events).
  5. Dự báo chuỗi sự kiện hoặc hành vi có khả năng tiếp diễn dựa trên các dấu vết chuyển trạng thái đã thu thập (determining events that are likely to follow).

Đối tượng và phạm vi nghiên cứu

  • Đối tượng nghiên cứu: Các hành vi tấn công xâm nhập hệ thống từ bên ngoài, hành vi lạm quyền từ bên trong (vấn đề nội bộ - insider problem), các chuỗi chuyển trạng thái thực thi của phần mềm ở không gian người dùng (user space) và không gian nhân (kernel space).
  • Phạm vi không gian và hệ thống: Các hệ thống máy tính đơn bộ xử lý (uniprocessor) kiến trúc x86 chạy hệ điều hành dạng UNIX (cụ thể là FreeBSD 5.4 và Fedora Core 4). Dữ liệu phân tích tập trung vào các chương trình viết bằng ngôn ngữ C/C++.
  • Giới hạn phạm vi: Luận án không bao gồm các thao tác can thiệp trực tiếp vào phần cứng vật lý, không giải quyết các sự kiện diễn ra thuần túy bên trong môi trường máy ảo phần mềm (như Java Virtual Machine - JVM), đồng thời không đi sâu vào khía cạnh thủ tục pháp lý tố tụng (chuỗi bảo quản chứng cứ số - chain of custody) hay kỹ thuật phục hồi dữ liệu đã xóa trên thiết bị lưu trữ.

Tổng quan tài liệu và vị trí của luận án

Các hướng nghiên cứu trước

Tác giả Sean Philip Peisert đã tổng hợp và phân loại các công trình nghiên cứu tiền đề theo các nhóm tiếp cận:

  1. Nền tảng kiểm toán và vết nhật ký:

    • Anderson (1980): Công trình đầu tiên đề xuất việc sử dụng vết kiểm toán (audit trails) phục vụ giám sát an ninh.
    • Bonyun (1980): Phân tích giá trị của dữ liệu kiểm toán và vị trí đặt các cơ chế thu thập dữ liệu, nhưng chưa khái quát hóa được quy trình lựa chọn dữ liệu.
    • Bishop (1988a, 1989, 1995, 2003): Nghiên cứu cấu trúc dữ liệu nhật ký, kiểm toán tệp tin, phân loại kiểm toán dựa trên trạng thái (state-based) và chuyển trạng thái (transition-based), cũng như giới hạn lý thuyết của việc kiểm toán trong thực thi chính sách an ninh.

  2. Các công cụ và giải pháp thu thập nhật ký truyền thống:

    • Allman (2005): Khảo sát giao thức syslog trong UNIX, nhấn mạnh bản chất của syslog là phục vụ gỡ lỗi ứng dụng, không được thiết kế cho mục đích an ninh.
    • Sun Microsystems (2001): Mô-đun an ninh cơ bản BSM (Basic Security Module) trên nền tảng Solaris, ghi nhận các sự kiện mức hệ thống dựa trên giả định chủ quan.
    • Tiếp cận dạng "hộp công cụ" (toolbox) kết hợp các công cụ chuyên biệt: Tripwire (Kim & Spafford, 1994) ghi nhận thay đổi tệp tin; The Coroner’s Toolkit - TCT (Farmer & Venema, 2004; Venema & Farmer) phân tích trạng thái tĩnh và tệp tin; TCP Wrappers (Venema, 1992) giám sát kết nối mạng.

  3. Truy vết sự kiện và tái dựng hành vi dựa trên máy ảo và lời gọi hệ thống:

    • Dunlap cùng các cộng sự (2002): Hệ thống ReVirt sử dụng máy ảo để ghi nhận sự kiện không đơn định (non-deterministic logging) phục vụ việc tái phát lại tất định (deterministic replay).
    • King & Chen (2005): Hệ thống BackTracker sử dụng đồ thị phụ thuộc của các lời gọi hệ thống (system calls) để tái dựng chuỗi tiến trình và tệp tin liên quan đến cuộc xâm nhập. Các công trình kế thừa gồm Subhraveti & Volovich (2005), King cùng các cộng sự (2005).
    • Goel cùng các cộng sự (2005): Hệ thống Forensix thu thập toàn bộ lời gọi hệ thống và lưu trữ vào cơ sở dữ liệu để phục vụ truy vấn sau sự cố.

  4. Mô hình hóa pháp chứng và kiểm toán hình thức:

    • Gross (1997): Hình thức hóa việc phân tích sự khác biệt giữa các trạng thái hệ thống để suy diễn các hành vi đã diễn ra trên hệ thống nguyên bản.
    • Schneider (2000): Mô hình hóa các cơ chế giám sát thực thi an ninh (security automata).
    • Kupiec (2004): Đánh giá tác động hiệu năng của các phương pháp kiểm toán theo các khung thời gian khác nhau (thời gian thực, gần thời gian thực, định kỳ, lưu trữ).
    • Templeton & Levitt (2000) và Ning cùng các cộng sự (2007): Mô hình requires/provides trong phát hiện tấn công nhiều giai đoạn (multi-stage attacks).
    • Forrest cùng các cộng sự (1996, 1999) và Tan & Maxion (2002): Phát hiện bất thường dựa trên chuỗi lời gọi hệ thống bằng phương pháp học máy dựa trên cá thể (instance-based learning) và khoảng cách Hamming.

Khoảng trống luận án lựa chọn giải quyết

Các công trình trước đây hoặc chỉ khai thác dữ liệu có sẵn (available data) ở mức trừu tượng cao, hoặc ghi nhận toàn bộ mọi sự kiện ở mức chỉ lệnh máy dẫn đến chi phí tài nguyên quá lớn. Các hệ thống như BackTracker hay Forensix tập trung vào lời gọi hệ thống (system calls), vốn chỉ phản ánh tương tác giữa tiến trình với hạt nhân (kernel) mà bỏ qua ngữ cảnh bên trong không gian người dùng. Ngược lại, việc ghi nhận toàn bộ các lệnh hợp ngữ tạo ra từ 1.000 đến 10.000 lệnh cho mỗi lời gọi hệ thống, làm bùng nổ dữ liệu lưu trữ.

Luận án của Peisert giải quyết khoảng trống này bằng cách: (1) Đưa ra mức trừu tượng trung gian thông qua chuỗi lời gọi hàm (sequences of function calls) trong không gian người dùng kết hợp không gian nhân; (2) Xây dựng mô hình toán học hình thức Laocoön dựa trên mô hình requires/provides để chứng minh toán học và xác định tập dữ liệu tối thiểu nhưng đầy đủ cần ghi vết dựa trên đồ thị mục tiêu tấn công.

Cơ sở lý thuyết và phương pháp nghiên cứu

Cơ sở lý thuyết và khung phân tích

Luận án kết hợp các nền tảng lý thuyết và nguyên tắc thiết kế sau:

  1. Phân loại kiểm toán chuyển trạng thái (Transition-based Logging): Luận án chứng minh rằng kiểm toán dựa trên trạng thái (chụp ảnh hệ thống định kỳ) không phù hợp cho an toàn thông tin vì không thể tái phát lại tất định các sự kiện đơn lẻ khi các dấu vết bị xóa giữa hai chu kỳ chụp. Do đó, kiểm toán dựa trên sự kiện và chuyển trạng thái là lựa chọn bắt buộc.
  2. Năm nguyên tắc phân tích pháp chứng (Five Principles of Forensic Analysis):
    • Nguyên tắc 1: Xem xét toàn bộ hệ thống (Consider the entire system).
    • Nguyên tắc 2: Ghi vết thông tin không phụ thuộc vào các giả định chủ quan (Log information without regard to assumptions).
    • Nguyên tắc 3: Xem xét các hệ quả, không chỉ các hành động (Consider the effects, not just the actions).
    • Nguyên tắc 4: Xem xét ngữ cảnh để hỗ trợ khả năng thấu hiểu (Consider context to assist in understanding).
    • Nguyên tắc 5: Trình bày và xử lý hành động cùng kết quả theo phương thức dễ hiểu đối với con người (Present and process actions and results in an understandable way).
  3. Mô hình Laocoön (Goal-Oriented Logging Model): Xây dựng dựa trên mô hình requires/provides. Luận án mô hình hóa cuộc tấn công dưới dạng đồ thị có hướng (attack graph). Kẻ tấn công có thể sử dụng vô số phương thức khai thác lỗ hổng (exploit) không thể dự đoán trước ở giai đoạn giữa, nhưng điểm khởi đầu và mục tiêu cuối cùng (goals/sub-goals) luôn hội tụ về một số trạng thái giới hạn. Mô hình áp dụng hàm $\lambda$ để phân rã đồ thị và xác định các thuộc tính dịch vụ (service properties) cần ghi vết.
+------------------------------------------------------------------------------------+
|                                    MÔ HÌNH LAOCOÖN                                 |
|                                                                                    |
|  [Khởi đầu cuộc tấn công]  --->  [Khai thác chưa biết]  --->  [Mục tiêu kẻ tấn công]  |
|      (Điểm hội tụ đầu)           (Bùng nổ phương thức)           (Điểm hội tụ cuối)   |
|              |                                                          |          |
|              +----------------> [ Hàm trích xuất lambda ] <-------------+          |
|                                         |                                          |
|                                         v                                          |
|                       [ Tập dữ liệu tối thiểu cần ghi vết ]                         |
+------------------------------------------------------------------------------------+

Phương pháp nghiên cứu thực nghiệm

  • Học máy dựa trên cá thể (Instance-based Machine Learning): Phân tích các chuỗi lời gọi hàm có độ dài cố định $k$ ($1 \le k \le 20$). So sánh các chuỗi trong quá trình thực thi cần kiểm tra với cơ sở dữ liệu các chuỗi thực thi an toàn (safe corpus) thông qua khoảng cách Hamming.
  • Công cụ đo lường động (Dynamic Binary Instrumentation):
    • Sử dụng công cụ Pin của Intel trên hệ điều hành FreeBSD 5.4 để chèn mã theo dõi động mà không cần biên dịch lại mã nguồn, ghi nhận toàn bộ lời gọi hàm và các điểm trả về của hàm (-RET).
    • Sử dụng công cụ ltrace trên hệ điều hành Fedora Core 4 để theo dõi các lời gọi thư viện liên kết động, cho phép trích xuất tham số truyền vào và giá trị trả về của hàm.

Nguồn tư liệu và dữ liệu thực nghiệm

Dữ liệu phân tích được thu thập từ các phần mềm hệ thống thực tế trên nền tảng UNIX và các tình huống khai thác an ninh kinh điển:

  • Tiện ích chuyển đổi người dùng su (mô phỏng loại bỏ và bỏ qua kiểm tra mật khẩu qua PAM).
  • Trình khách ssh của OpenSSH (mô phỏng phần mềm gián điệp đánh cắp mật khẩu hiển thị ra màn hình hoặc gửi qua socket mạng - tái hiện cuộc tấn công có thật tại Trung tâm Siêu máy tính San Diego - SDSC giai đoạn 2004–2005).
  • Tiện ích in ấn lpr (lỗ hổng ghi đè tệp tin /etc/passwd).
  • Chương trình kiểm tra lỗ hổng tràn bộ đệm (buffer overflow).
  • Chương trình gọi tiện ích hệ thống thông qua popen (mô phỏng lỗ hổng Trojan horse trên biến môi trường đường dẫn PATH của trình biên tập vi).

Nội dung chính theo từng chương

Chương 1: Giới thiệu (Introduction)

Chương 1 thiết lập bối cảnh, định nghĩa các khái niệm cơ bản của phân tích pháp chứng, ghi vết và kiểm toán. Tác giả nêu bật luận điểm: việc gia tăng dữ liệu ghi vết không đồng nghĩa với việc gia tăng độ chính xác phân tích nếu dữ liệu thu thập không đúng trọng tâm. Chương này trình bày mô hình không gian đánh đổi giữa chi phí thu thập và giá trị sử dụng pháp chứng (forensic utility), đồng thời xác định mục tiêu của luận án là đạt được giá trị pháp chứng cao với lượng dữ liệu tối ưu bằng phương pháp tiếp cận có mô hình hướng dẫn.

Chương 2: Các công trình liên quan (Related Work)

Chương 2 phân tích toàn diện lịch sử phát triển của các hệ thống kiểm toán từ năm 1980 đến năm 2007. Tác giả so sánh chi phí hiệu năng và dung lượng dữ liệu của các phương pháp hiện hành:

  • Một sự cố an ninh tại San Diego Supercomputer Center (SDSC) tạo ra gần 3 GB dữ liệu syslog trong 1 tuần với 28.634.491 dòng nhật ký.
  • Hệ thống ReVirt tạo ra ít nhất 1,4 GB dữ liệu/ngày với độ suy giảm hiệu năng CPU lên tới 68%.
  • Hệ thống BackTracker tạo ra 1,2 GB dữ liệu/ngày với độ suy giảm hiệu năng CPU lên tới 38%.
  • Tỷ lệ các lời gọi hệ thống (system calls) chỉ chiếm từ 0,5% đến 5% tổng số lời gọi hàm (function calls), dẫn đến việc ghi nhận toàn bộ lời gọi hàm làm tăng dung lượng lưu trữ từ 20 đến 200 lần so với chỉ ghi system calls. Tuy nhiên, mức độ trừu tượng của lời gọi hàm cung cấp ngữ cảnh giải thích vượt trội cho con người.

Chương 3: Phương pháp phân tích pháp chứng sử dụng chuỗi lời gọi hàm (A Method of Forensic Analysis Using Sequences of Function Calls)

Chương 3 trình bày chi tiết phương pháp phát hiện bất thường hậu kiểm dựa trên chuỗi lời gọi hàm và đánh giá qua các thực nghiệm cụ thể.

1. Thực nghiệm với tiện ích su

  • Loại bỏ hàm xác thực pam_authenticate: So sánh bản gốc (su-orig) và bản chỉnh sửa (su-mod). Khi chọn độ dài chuỗi $k=4$, su-orig ghi nhận 37.142 chuỗi (2.136 chuỗi phân biệt), trong khi su-mod có 8.630 chuỗi (1.812 chuỗi phân biệt). Số chuỗi chỉ xuất hiện trong su-mod là 46 chuỗi. Phân tích tần suất chuỗi trong su-orig chỉ ra 14 chuỗi chiếm gần 50% thời gian thực thi của chương trình đều liên quan trực tiếp đến các hàm băm và mã hóa MD5 (MD5Update, MD5Init, MD5Pad, MD5Final, memcpy), cung cấp manh mối trực tiếp về việc cơ chế xác thực bị can thiệp.
Chuỗi lời gọi hàm ($k=4$) chỉ có ở su-orig Số lần xuất hiện Tỷ lệ trong chương trình
MD5Update, memcpy, MD5Update, memcpy 3.533 9,51%
memcpy, MD5Update, memcpy, MD5Update 1.528 4,11%
MD5Final, MD5Pad, MD5Update, memcpy 1.002 2,70%
memcpy, MD5Update, memcpy, memcpy 1.002 2,70%
memcpy, memcpy, memcpy, memcpy 1.002 2,70%
MD5Update, memcpy, memcpy, memcpy 1.002 2,70%
MD5Init, MD5Update, memcpy, MD5Update 1.002 2,70%
MD5Pad, MD5Update, memcpy, MD5Update 1.002 2,70%
memcpy, MD5Update, memcpy, MD5Final 1.001 2,70%
memcpy, MD5Final, MD5Pad, MD5Update 1.001 2,70%
MD5Update, memcpy, MD5Final, MD5Pad 1.001 2,70%
memcpy, memcpy, memset, MD5Init 1.000 2,69%
memcpy, memcpy, MD5Init, MD5Update 1.000 2,69%
memcpy, MD5Init, MD5Update, memcpy 1.000 2,00%
  • Bỏ qua kết quả trả về của pam_authenticate: Khi $k=2$, có 13 chuỗi phân biệt chỉ xuất hiện ở bản gốc, trong đó chuỗi strcmp, pam_set_item chỉ ra rằng kết quả xác thực không được thiết lập sau bước so sánh chuỗi. Nếu chỉ kiểm tra system calls, các chuỗi ghi nhận được (ioctl, close, setpgid, ioctl, sigaction, close) không phản ánh được bản chất logic xác thực bị bỏ qua.

2. Thực nghiệm với phần mềm gián điệp trên ssh

  • Hiển thị mật khẩu ra màn hình: Với $k=4$ và bổ sung điểm trả về của hàm (-RET), hàm read_passphrase xuất hiện rõ nét trong các chuỗi dị thường (memset-RET, read_passphrase-RET, input_userauth_info_req, packet_put_cstring).
  • Gửi mật khẩu qua socket mạng: Với $k=2$, phân tích phát hiện các lời gọi hàm mạng bất thường kết hợp với đọc mật khẩu: inet_aton, inet_addr, socket, sendto (ví dụ: chuỗi sendto-RET, read_passphrase).

3. Thực nghiệm khai thác quyền tệp tin trên lpr

Tái hiện lỗi ghi đè tệp tin /etc/passwd. Với $k=2$, hệ thống phát hiện 38 chuỗi phân biệt bất thường trong bản bị khai thác. Lời gọi hàm copy trong mã nguồn lpr.c làm lộ diện việc gọi hàm hệ thống lỗi thời creat (gây điều kiện tranh định vị race condition), dẫn tới các hệ quả bất thường như gọi lặp lại sys_unlink và seteuid.

4. Thực nghiệm tràn bộ đệm (Buffer Overflow)

Chương trình kiểm tra thực hiện sao chép chuỗi vượt quá 500 byte chứa shellcode chiếm quyền root. Kết quả phân tích chuỗi hàm có kèm điểm trả về cho thấy bản bị khai thác dừng ngay sau khi kết thúc hàm main (chuỗi vprintf-RET, printf-RET, main-RET), bỏ qua hoàn toàn hàm hệ thống exit và các hàm dọn dẹp tài nguyên tiêu chuẩn.

5. Thực nghiệm ngựa lừa (Trojan Horse qua biến PATH)

Chương trình sử dụng popen("date", "r") với biến môi trường PATH chứa thư mục hiện hành . trước /bin. Sử dụng ltrace với $k=6$, phân tích phát hiện các chuỗi gọi xstat64 kiểm tra thư mục hiện hành trả về giá trị 0 khi tìm thấy file date giả mạo, dừng tìm kiếm tiếp trong /bin, làm nổi bật sự khác biệt về đường dẫn tìm kiếm nhị phân.

Chương 4: Hướng tới các mô hình pháp chứng (Toward Forensic Models)

Chương 4 phân tích sâu 5 nguyên tắc phân tích pháp chứng, chỉ ra các khiếm khuyết của các hệ sinh thái ghi nhật ký đương thời và đề xuất các tiêu chuẩn chất lượng (qualities) mà một mô hình pháp chứng cần phải đáp ứng: tính đầy đủ (completeness), tính cần thiết (necessity), tính khả thi trong triển khai, và khả năng hỗ trợ trực tiếp nhận thức của chuyên gia điều tra.

Chương 5: Laocoön: Mô hình pháp chứng (Laocoön: The Forensic Model)

Chương 5 giới thiệu chi tiết mô hình hình thức Laocoön.

  • Mô hình định nghĩa các mục tiêu tấn công dưới dạng các bộ trạng thái và vị từ an ninh.
  • Phân tách đồ thị tấn công thành các nút mục tiêu đã biết (known goals) và các nút khai thác trung gian chưa biết (unknown exploits).
  • Sử dụng thuật toán giới hạn ranh giới các mục tiêu chưa biết và áp dụng hàm $\lambda$ để trích xuất danh mục các thuộc tính dịch vụ (service properties) cần ghi nhật ký.
  • Định nghĩa khái niệm Định danh đường dẫn duy nhất (Unique Path Identifier) nhằm bảo đảm rằng mọi đường dẫn thực thi dẫn tới trạng thái mục tiêu đều có thể phân biệt được thông qua dữ liệu nhật ký.
  • Trình bày chứng minh toán học về tính đầy đủ và tính cần thiết của mô hình.
+------------------------------------------------------------------------------------+
|                         BẢNG 5.3: CÁC LOẠI THUỘC TÍNH DỊCH VỤ                      |
|                                                                                    |
|  - Quyền truy cập tệp tin (File Access Permissions)                               |
|  - Trạng thái định danh tiến trình (UID / EUID / GID / EGID)                       |
|  - Ngữ cảnh thực thi và không gian địa chỉ bộ nhớ (Execution Context / Memory)      |
|  - Trạng thái kết nối và cổng truyền thông mạng (Network Socket State)             |
|  - Tính toàn vẹn cấu hình dịch vụ hệ thống (Service Configuration Integrity)       |
+------------------------------------------------------------------------------------+

Chương 6: Các ví dụ sử dụng Laocoön (Examples of Using Laocoön)

Chương 6 áp dụng mô hình Laocoön vào việc xây dựng đồ thị tấn công và suy diễn yêu cầu ghi vết cho hàng loạt kịch bản an ninh thực tế:

  • Chiếm quyền điều khiển shell root từ xa (Obtaining a Root Shell).
  • Chỉnh sửa tệp cấu hình mật khẩu /etc/passwd thông qua lỗi của tiện ích lpr.
  • Thay đổi đường dẫn tìm kiếm nhị phân PATH để thực thi mã độc.
  • Vượt qua các giao diện kiểm soát tiêu chuẩn thông qua lỗi ghi đè tệp tin ghi nhận đăng nhập utmp.
  • Lỗi kiểm tra tham số không nhất quán trong các tiện ích đổi shell chsh hoặc đổi thông tin cá nhân chfn.
  • Tiêm mã độc vào bộ nhớ dùng chung (Shared Memory Code Injection).
  • Đồ thị tấn công của sâu Internet Worm năm 1988 (Morris Worm).
  • Đồ thị tấn công của sâu Christma Exec Worm trên hệ thống máy chủ lớn.
  • Các lớp lỗ hổng trên hệ thống tệp tin mạng Network File System (NFS).

Chương 7: Hiện thực hóa, thực nghiệm và kết quả (Implementation, Experiments, and Results)

Chương 7 trình bày việc triển khai thực tế mô hình Laocoön trên hệ thống UNIX và kiểm chứng khả năng tái dựng các cuộc tấn công đã nêu trong Chương 6. Tác giả chứng minh rằng bằng cách áp dụng kỹ thuật loại bỏ đường dẫn (path elimination), hệ thống ghi nhận giảm thiểu đáng kể khối lượng dữ liệu log phát sinh trong khi vẫn bảo đảm cung cấp đầy đủ bằng chứng xác thực để kết luận nguyên nhân sự cố.

Chương 8: Đưa Laocoön từ mô hình thành hệ thống (Taking Laocoön from a Model to a System)

Chương 8 thảo luận các thách thức khi chuyển hóa mô hình lý thuyết sang một hệ thống vận hành tự động trong thực tế:

  • Vấn đề đo kiểm hệ thống (instrumentation), chi phí lưu trữ và xử lý dữ liệu log.
  • Quy trình tự động khám phá và biên dịch chính sách an ninh (Policy Discovery and Compilation), cùng kỹ thuật dịch ngược chính sách (Reverse-Engineering Policies) từ các hệ thống đang hoạt động.
  • Tính đầy đủ và tính cần thiết trong thực tế triển khai phần mềm và phần cứng.
  • Khả năng ứng dụng chéo giữa kỹ thuật phân tích pháp chứng và các hệ thống phát hiện xâm nhập (IDS).

Chương 9: Kết luận (Conclusions)

Chương 9 đúc kết các kết quả đạt được của luận án, khẳng định tính khả thi của việc mô hình hóa hình thức hoạt động ghi vết pháp chứng và phác thảo lộ trình phát triển trong tương lai.

Kết quả và những đóng góp mới

Đóng góp về mặt lý luận

  1. Hình thức hóa phân tích pháp chứng: Luận án là một trong những công trình tiên phong chuyển đổi phân tích pháp chứng máy tính từ trạng thái kinh nghiệm mang tính tùy tiện sang một ngành khoa học có mô hình toán học và phương pháp luận rõ ràng.
  2. Xây dựng 5 nguyên tắc cơ bản của phân tích pháp chứng: Đưa ra khung quy chuẩn định hướng cho việc thiết kế, xây dựng và đánh giá các cơ chế ghi vết và kiểm toán an ninh trên hệ điều hành.
  3. Mô hình Laocoön: Phát triển thành công mô hình ghi nhật ký định hướng mục tiêu dựa trên mô hình requires/provides, cung cấp chứng minh toán học về tính đầy đủ và tính cần thiết của dữ liệu pháp chứng.

Đóng góp về mặt thực tiễn

  1. Phương pháp phân tích chuỗi lời gọi hàm: Chứng minh thực nghiệm rằng việc theo dõi chuỗi lời gọi hàm ($1 \le k \le 10$) kết hợp với điểm trả về của hàm (-RET) trong không gian người dùng mang lại mức độ mô tả ngữ cảnh tối ưu cho chuyên gia điều tra, vượt trội so với việc chỉ theo dõi lời gọi hệ thống riêng lẻ.
  2. Tối ưu hóa dung lượng lưu trữ nhật ký: Cung cấp giải pháp cho phép loại bỏ dữ liệu dư thừa và dữ liệu gây nhiễu, giúp giảm tải dung lượng nhật ký cần kiểm toán nhưng vẫn bảo đảm đầy đủ dữ liệu để tái dựng chính xác đường dẫn tấn công.
  3. Khung thực nghiệm đa dạng: Xây dựng và kiểm chứng thành công phương pháp trên nhiều lớp lỗ hổng an ninh kinh điển trên hệ điều hành UNIX (tràn bộ đệm, leo thang đặc quyền, giả mạo đường dẫn, can thiệp xác thực PAM, phần mềm gián điệp mạng).

Kiến nghị và giải pháp đề xuất

  • Tích hợp cơ chế ghi vết định hướng mục tiêu ngay từ giai đoạn thiết kế kiến trúc hệ điều hành và phần mềm, thay vì dựa vào các giải pháp bổ sung chắp vá sau khi hệ thống đã hoàn thiện.
  • Kết hợp chính sách an ninh của tổ chức với bộ biên dịch chính sách để tự động cấu hình các điểm chèn mã theo dõi trên hệ thống.
  • Sử dụng độ dài chuỗi phân tích $k$ linh hoạt ($k=2$ hoặc $k=4$) trong các công cụ hỗ trợ điều tra pháp chứng để cân bằng giữa khối lượng thông tin hiển thị và khả năng nhận diện bất thường của con người.

Hạn chế và hướng nghiên cứu tiếp

Hạn chế được ghi nhận trong văn bản

  • Hạn chế của công cụ đo kiểm Pin: Do giới hạn kỹ thuật, công cụ đo kiểm động Pin đôi khi bỏ lỡ dưới 1% tổng số lời gọi hàm thực tế.
  • Quan sát mã chèn bộ nhớ trong tràn bộ đệm: Công cụ Pin đòi hỏi phải thực thi các lệnh chuyên biệt giữa thời điểm ghi mã lên ngăn xếp (stack) và thời điểm thực thi mã để có thể đo kiểm mã động, điều này làm biến dạng góc nhìn trực tiếp đối với bản thân shellcode; do đó việc phân tích chủ yếu dựa vào quan sát hệ quả gián tiếp (tiến trình bỏ qua lệnh exit).
  • Phụ thuộc vào hệ thống đơn bộ xử lý: Việc phân tích tái phát lại tất định trên máy ảo gặp trở ngại trên hệ thống đa bộ xử lý (multiprocessor) do không thể xác định thứ tự các thao tác đọc/ghi đồng thời trên bộ nhớ dùng chung giữa các luồng xử lý độc lập.
  • Tự động hóa chính sách: Quy trình trích xuất mục tiêu tấn công từ chính sách an ninh trong luận án phần lớn vẫn được thực hiện thủ công, chưa hoàn toàn tự động hóa.

Hạn chế suy diễn từ phạm vi nghiên cứu

  • Nghiên cứu tập trung vào các hệ thống dạng UNIX/C/C++, chưa mở rộng đánh giá thực nghiệm trên các hệ điều hành thương mại đóng mã nguồn (như Microsoft Windows) hoặc các ngôn ngữ bậc cao có môi trường thực thi quản lý bộ nhớ tự động.

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

  • Ứng dụng mô hình Markov ẩn (Hidden Markov Models - HMMs) và các kỹ thuật khai phá dữ liệu (data mining) để tự động hóa việc phân loại chuỗi lời gọi hàm bất thường.
  • Nghiên cứu phát triển các công cụ ghi vết có khả năng chống giả mạo (tamper-proof logging).
  • Mở rộng phân tích bất thường từ cấp độ tiến trình đơn lẻ lên cấp độ toàn bộ phiên làm việc (sessions) và hành vi người dùng (users).
  • Hoàn thiện khung kỹ nghệ đảo ngược chính sách (Reverse-Engineering Policies) và biên dịch chính sách an ninh tự động phục vụ cấu hình ghi nhật ký.

Giá trị tham khảo

Đối tượng thụ hưởng

  • Nghiên cứu sinh và Giảng viên: Cung cấp nền tảng lý thuyết hình thức về mô hình hóa phân tích pháp chứng máy tính, phương pháp thiết kế thực nghiệm an ninh thông tin và các bài học kinh nghiệm trong kiểm toán hệ điều hành.
  • Chuyên viên phân tích pháp chứng số và Ứng cứu sự cố (DFIR): Nắm bắt phương pháp luận phân tích chuỗi lời gọi hàm để xác định vị trí mã nguồn bị can thiệp khi phân tích mã độc hoặc điều tra các cuộc tấn công tinh vi.
  • Quản trị viên hệ thống và Chuyên gia an ninh mạng: Hiểu rõ các nguyên tắc lựa chọn dữ liệu ghi vết, khắc phục sự lãng phí tài nguyên khi lưu trữ nhật ký và biết cách cấu hình hệ thống ghi nhận đúng các dữ liệu trọng yếu.
  • Nhà phát triển hệ điều hành và phần mềm an ninh: Tham khảo khung mô hình Laocoön để thiết kế các giao diện lập trình và kiến trúc hạt nhân hỗ trợ sẵn khả năng thu thập dữ liệu pháp chứng.

Phần nội dung đáng tham khảo đặc biệt

  • Chương 3: Phương pháp phân tích chuỗi lời gọi hàm và kỹ thuật xử lý điểm trả về của hàm (-RET) để phát hiện can thiệp mã nguồn.
  • Chương 4: Năm nguyên tắc phân tích pháp chứng và tiêu chuẩn thiết kế mô hình kiểm toán.
  • Chương 5 & 6: Khung toán học của mô hình Laocoön và phương pháp xây dựng đồ thị tấn công chi tiết cho các lỗ hổng hệ thống.

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

1. Tại sao việc ghi nhận chuỗi lời gọi hàm lại có giá trị phân tích pháp chứng cao hơn so với chỉ ghi nhận lời gọi hệ thống?

Lời gọi hệ thống (system calls) chỉ phản ánh tương tác giữa tiến trình với nhân hệ điều hành và có tính chất kỹ thuật thuần túy (ví dụ: ioctl, setpgid, write), khiến chuyên gia phân tích khó xác định vị trí lỗi logic trong mã nguồn. Lời gọi hàm (function calls) bao quát cả không gian người dùng lẫn không gian nhân, mang tính mô tả ngữ cảnh rõ ràng hơn (ví dụ: pam_authenticate, read_passphrase, MD5Update). Mặc dù tổng số lời gọi hàm lớn hơn từ 20 đến 200 lần so với system calls, số chuỗi bất thường khác biệt mà chuyên gia cần trực tiếp kiểm tra chỉ tăng khoảng 7 lần hoặc dung lượng hiển thị tăng khoảng 50%, giúp định vị chính xác đoạn mã nguồn bị xâm phạm.

2. Sự khác biệt cốt lõi giữa kiểm toán dựa trên trạng thái (state-based) và kiểm toán dựa trên chuyển trạng thái (transition-based) trong an ninh là gì?

Kiểm toán dựa trên trạng thái thu thập thông tin bằng cách lấy mẫu định kỳ hoặc chụp ảnh toàn bộ trạng thái hệ thống tại các thời điểm ngắt. Phương pháp này mang tính tùy tiện về tần suất và có nguy cơ bỏ sót hoàn toàn cuộc tấn công nếu kẻ tấn công xâm nhập và xóa dấu vết giữa hai chu kỳ chụp ảnh. Kiểm toán dựa trên chuyển trạng thái ghi nhận các sự kiện cụ thể kích hoạt sự biến đổi trạng thái của hệ thống. Do trong điều tra an ninh không thể tái lập lại một cuộc tấn công ngẫu nhiên nếu không dùng kỹ thuật tái phát lại tất định, kiểm toán dựa trên chuyển trạng thái là phương pháp duy nhất đảm bảo ghi nhận được dấu vết sự kiện chỉ xuất hiện một lần.

3. Mô hình Laocoön giải quyết vấn đề bùng nổ phương thức tấn công ở giai đoạn giữa cuộc tấn công như thế nào?

Trong một cuộc tấn công nhiều giai đoạn, kẻ tấn công có thể sử dụng vô số phương thức khai thác lỗ hổng (exploit) khác nhau mà hệ thống không thể dự đoán trước ở giai đoạn giữa. Tuy nhiên, điểm khởi đầu và mục tiêu cuối cùng (goals/sub-goals) của cuộc tấn công luôn có tính hội tụ cao về một số trạng thái giới hạn (ví dụ: chiếm shell root, ghi đè tệp tin đặc quyền, gửi dữ liệu qua mạng). Mô hình Laocoön chỉ mô hình hóa các trạng thái mục tiêu đã biết ở hai đầu và áp dụng hàm toán học $\lambda$ để xác định các thuộc tính dịch vụ cần thiết lập ranh giới kiểm soát, từ đó thu thập đủ dữ liệu để tái dựng các bước khai thác trung gian chưa biết mà không cần phải mô hình hóa toàn bộ các kỹ thuật khai thác đó.

4. Tại sao việc bổ sung thông tin điểm trả về của hàm (function returns) lại quan trọng trong một số thực nghiệm?

Trong nhiều trường hợp thực nghiệm (như phân tích trình khách ssh bị sửa đổi hoặc lỗi tràn bộ đệm), chỉ theo dõi điểm bắt đầu gọi hàm không đủ để phân biệt hành vi bất thường khi các hàm được gọi có tên gọi phức tạp hoặc trùng lặp với luồng thực thi an toàn. Việc bổ sung điểm trả về của hàm (ký hiệu -RET) giúp xác định thứ tự thực thi chính xác của cấu trúc lồng nhau giữa các hàm, làm lộ diện các hàm quan trọng bị chèn vào giữa luồng (như read_passphrase) hoặc phát hiện việc tiến trình kết thúc bất thường mà không gọi các hàm dọn dẹp tiêu chuẩn và hàm hệ thống exit.

5. Tại sao kỹ thuật tái phát lại tất định (deterministic replay) trên máy ảo gặp trở ngại trên hệ thống đa bộ xử lý?

Kỹ thuật tái phát lại tất định trên máy ảo đòi hỏi phải ghi nhận và tái lập chính xác thứ tự của mọi sự kiện không đơn định. Trên hệ thống đa bộ xử lý (multiprocessor), các luồng thực thi chạy song song trên các vi xử lý khác nhau có thể thực hiện đồng thời các thao tác đọc và ghi vào cùng một vị trí bộ nhớ dùng chung (shared memory). Cả phần mềm giám sát máy ảo (hypervisor) lẫn hệ điều hành đều không thể xác định chính xác tuyệt đối thứ tự thời gian của các truy cập bộ nhớ đồng thời này, dẫn đến sự tích lũy sai lệch qua các lần phát lại và làm mất đi tính chính xác của dữ liệu ghi nhận ban đầu.

Kết luận

Luận án tiến sĩ của Sean Philip Peisert đã đặt nền móng lý thuyết hình thức quan trọng cho lĩnh vực phân tích pháp chứng máy tính thông qua việc xây dựng mô hình ghi nhật ký định hướng mục tiêu Laocoön. Bằng việc chứng minh toán học và thực nghiệm trên các hệ thống UNIX thực tế, tác giả khẳng định việc phân tích chuỗi lời gọi hàm ở mức độ trừu tượng thích hợp mang lại hiệu quả vượt trội trong việc tái dựng các cuộc xâm nhập so với các phương pháp kiểm toán truyền thống. Nghiên cứu cung cấp một phương pháp luận khoa học chặt chẽ giúp tối ưu hóa tài nguyên ghi vết hệ thống, hỗ trợ đắc lực cho công tác điều tra an ninh và định hướng cho việc thiết kế các hệ điều hành an toàn trong tương lai.