Tổng quan về luận án

Sự bùng nổ của các hệ thống phần mềm dựa trên nền tảng web trong các lĩnh vực trọng yếu như y tế, tài chính, giáo dục và quốc phòng đặt ra những thách thức an ninh chưa từng có. Báo cáo của Symantec (2019) chỉ ra rằng các vụ tấn công nhắm vào ứng dụng web chiếm tới 56% tổng số vụ vi phạm an ninh mạng toàn cầu. Nghiên cứu của Viện Ponemon (2017) trên 419 doanh nghiệp thuộc 13 quốc gia cũng xác nhận thiệt hại trung bình cho một vụ rò rỉ dữ liệu lên tới 3,62 triệu USD (tương đương 141 USD cho mỗi bản ghi bị đánh cắp), trong khi sự cố rò rỉ thông tin cá nhân của 70 triệu khách hàng tại Tập đoàn Target (Mỹ) năm 2013 đã tiêu tốn hơn 300 triệu USD chi phí khắc phục. Kiểm soát truy cập (Access Control) là tuyến phòng thủ cốt lõi để đảm bảo bộ ba tính chất an ninh C-I-A: Tính bảo mật (Confidentiality), Tính toàn vẹn (Integrity) và Tính sẵn sàng (Availability) theo chuẩn ISO/IEC 27002:2013 và ISO/IEC 27034:2011. Tuy nhiên, theo McGraw, khoảng 50% lỗ hổng an ninh xuất phát trực tiếp từ các khiếm khuyết trong thiết kế kiến trúc và sai sót lập trình.

Khoảng trống nghiên cứu (Research Gap) then chốt hiện nay nằm ở sự thiếu hụt các phương pháp tự động hóa có khả năng phát hiện sự sai lệch (mismatch) giữa đặc tả chính sách an ninh hình thức và mã nguồn triển khai thực tế trên cả hai mô hình Điều khiển truy cập dựa trên vai trò (RBAC) và Điều khiển truy cập dựa trên thuộc tính (ABAC), đặc biệt khi các chính sách này được phân tán theo cả phương pháp an ninh lập trình (Programmatic Security) lẫn an ninh khai báo (Declarative Security). Các nghiên cứu trước đây (như Koved et al., Al-Bataineh & Debbabi) chủ yếu tập trung vào phân tích tĩnh đơn lẻ hoặc kiểm thử động tại thời điểm chạy (runtime) vốn tốn kém tài nguyên và không thể bao quát toàn bộ không gian trạng thái.

Luận án tiến sĩ "Một số phương pháp kiểm chứng các chính sách điều khiển truy cập cho hệ thống phần mềm" của Nghiên cứu sinh Lương Thanh Nhạn (người hướng dẫn: PGS. Trương Ninh Thuận, Chuyên ngành Kỹ thuật phần mềm, Mã số: 9480103.01 tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội) giải quyết trực diện bài toán này. Nghiên cứu xác lập 3 câu hỏi nghiên cứu (Research Questions) và giả thuyết khoa học:

  • RQ1: Làm thế nào để trích xuất và kiểm chứng tự động các quy tắc RBAC triển khai bằng phương pháp an ninh lập trình trong kiến trúc MVC? (Giả thuyết H1: Việc kết hợp đồ thị khai thác tài nguyên và ma trận kiểm soát truy cập cho phép định vị 100% các vi phạm thừa/thiếu quyền cấp độ phương thức).
  • RQ2: Phương pháp hình thức nào giúp phát hiện xung đột giữa phép gán người dùng - vai trò ($UA$) và vai trò - quyền ($PA$) cùng ràng buộc cấp quyền (SecureUML) trong an ninh khai báo? (Giả thuyết H2: Mô hình cây phân tích quy tắc truy cập kết hợp truy vấn cơ sở dữ liệu sẽ thẩm định triệt để các ràng buộc phân chia nhiệm vụ SoD).
  • RQ3: Làm thế nào để xác minh sự phù hợp của chính sách ABAC triển khai qua ngôn ngữ biểu thức Spring (SpEL) đối với bộ ba tính chất C-I-A chỉ bằng phân tích mã nguồn tĩnh? (Giả thuyết H3: Khung đánh giá vị từ Boolean trên các thuộc tính chủ thể, tài nguyên và môi trường cho phép chứng minh hình thức tính bảo mật, toàn vẹn và sẵn sàng).

Phạm vi nghiên cứu tập trung vào các hệ thống web doanh nghiệp phát triển trên nền tảng JavaEE, kiến trúc Model-View-Controller (MVC) và khung làm việc Spring Security. Luận án đã tạo ra bước đột phá khi xây dựng thành công 3 công cụ kiểm chứng tự động: CheckingRBAC, VeRA và APVer, được thực nghiệm kiểm chứng thành công trên hệ thống quản lý hồ sơ y tế bệnh viện phức tạp.

Literature Review và Positioning

Nghiên cứu về kiểm chứng điều khiển truy cập trong kỹ nghệ phần mềm phát triển qua nhiều giai đoạn với các luồng lý thuyết chính:

                                   vs.
                                  Kiểm chứng tự động RBAC/ABAC trên JavaEE, Spring Security,
                                  Đồng bộ Mã nguồn - CSDL - Đặc tả hình thức (C-I-A Verification).

Tổng quan y văn phản ánh hai trường phái đối lập sâu sắc trong thẩm định an ninh phần mềm:

  1. Phân tích động (Dynamic Analysis) vs. Phân tích tĩnh (Static Analysis): Các học giả ủng hộ phân tích động (như Halfond et al.) cho rằng quan sát hành vi runtime cung cấp độ chính xác thực thi tuyệt đối, loại bỏ cảnh báo giả. Ngược lại, trường phái phân tích tĩnh (như Evans & Larochelle, 2002; Chess & McGraw, 2004) chứng minh phân tích động không thể bao quát toàn bộ các nhánh rẽ điều kiện (paths), trong khi phân tích tĩnh thông qua Cây cú pháp trừu tượng (AST) và Đồ thị luồng điều khiển (CFG) có khả năng bao phủ 100% không gian mã nguồn ngay từ giai đoạn phát triển (early SDLC), giúp giảm thiểu chi phí sửa lỗi theo cấp số nhân.
  2. An ninh khai báo (Declarative Security) vs. An ninh lập trình (Programmatic Security): An ninh khai báo (qua XML Deployment Descriptors hoặc Java Annotations như @PreAuthorize) mang tính trực quan, chuẩn hóa nhưng thiếu tính linh hoạt khi biểu diễn logic nghiệp vụ phức tạp. Ngược lại, an ninh lập trình cho phép can thiệp sâu vào logic nội tại của phương thức nhưng lại dễ gây phân tán mã an ninh, tạo ra các lỗ hổng tiềm ẩn do lập trình viên hiểu sai đặc tả thiết kế.

So sánh với các công cụ kiểm chứng quốc tế điển hình:

  • MOPS (Model checking Program for Security Properties - Chen & Wagner, 2002): Sử dụng ôtômat đẩy xuống (Pushdown Automaton - PDA) và ôtômat hữu hạn trạng thái (FSA) để kiểm tra trật tự lời gọi hàm API an toàn trong ngôn ngữ C. Tuy nhiên, MOPS không hỗ trợ các kiến trúc hướng đối tượng phức tạp như JavaEE MVC và không kiểm chứng được ngữ nghĩa phân quyền RBAC/ABAC.
  • SPlint (Secure Programming LINT - Evans & Larochelle, 2002): Phân tích luồng dữ liệu dựa trên các chú thích (annotations) trong mã C, yêu cầu lập trình viên phải tự viết chú thích thủ công – một điểm nghẽn lớn trong các dự án công nghiệp quy mô lớn.
  • GraphMatch (Al-Bataineh & Debbabi, 2010): Sử dụng Đồ thị phụ thuộc hệ thống (SDG) từ CodeSurfer để tìm kiếm các mẫu vi phạm chính sách an ninh nhưng chưa giải quyết được bài toán đối chiếu tự động giữa đặc tả chính sách đa cấp với cơ sở dữ liệu phân quyền thực tế.

Luận án của NCS. Lương Thanh Nhạn đã định vị chính xác khoảng trống học thuật này: Xây dựng một phương pháp luận toàn diện tích hợp trích xuất tĩnh đồ thị khai thác tài nguyên, phân tích cây quy tắc truy cập và biểu thức SpEL để kiểm chứng tự động cả RBAC và ABAC trên hệ thống JavaEE/Spring Security mà không phụ thuộc vào việc thực thi phần mềm.

Đóng góp lý thuyết và khung phân tích

Đóng góp cho lý thuyết

Luận án mở rộng trực tiếp ba nền tảng lý thuyết an ninh máy tính kinh điển:

  1. Lý thuyết RBAC96 (Sandhu et al., 1996): Mở rộng định lý gán quyền thông qua việc hình thức hóa mối quan hệ giữa các thành phần kiến trúc MVC (Model-View-Controller) với ma trận kiểm soát truy cập theo vai trò. Luận án chuyển hóa việc thẩm định vai trò từ cấp độ định danh người dùng sang cấp độ lời gọi phương thức thực thi tài nguyên cụ thể.
  2. Lý thuyết SecureUML (Basin, Doser & Lodderstedt, 2006): Phát triển mô hình biểu diễn các ràng buộc cấp quyền (Authorization Constraints) và phân chia nhiệm vụ (Separation of Duties - SoD) thành cấu trúc dữ liệu hình thức dạng Cây phân tích truy cập theo vai trò (Role-Based Access Parsing Tree), cho phép thuật toán hóa việc kiểm tra tính tương thích giữa mã nguồn và cơ sở dữ liệu quan hệ.
  3. Mô hình ABAC chuẩn NIST SP 800-162 (Hu et al., 2014): Thiết lập mô hình toán học hình thức đánh giá chính sách ABAC dưới dạng các hàm Boolean đa biến trên không gian thuộc tính $M_{ABAC} = \langle S, RS, E, A_s, A_{rs}, A_e, OP, P \rangle$, tạo ra khung lý thuyết đầu tiên chứng minh tĩnh bộ ba tính chất C-I-A mà không cần môi trường thực thi.
                      Đặc tả RBAC                      Đặc tả ABAC

Khung phân tích độc đáo

Khung phân tích của luận án tích hợp liên ngành giữa Lý thuyết Ngôn ngữ lập trình, Phân tích mã tĩnh và An ninh thông tin, thiết lập 3 mô hình biểu diễn trung gian độc đáo:

  • Đồ thị khai thác tài nguyên (Resource Extraction Graph): Biểu diễn luồng điều khiển và tương tác giữa Controller và View trong ứng dụng JavaEE, ánh xạ trực tiếp các thao tác create, read, update, delete vào các đối tượng dữ liệu được quản lý bởi Model.
  • Ma trận kiểm soát truy cập theo vai trò (Role-Based Access Control Matrix): Mô hình hóa toán học không gian phân quyền dưới dạng ma trận hai chiều giữa tập Vai trò ($Roles$) và tập Quyền ($Permissions = 2^{Operations \times Objects}$), đóng vai trò cấu trúc dữ liệu trung gian cho thuật toán so khớp tự động.
  • Cây phân tích quy tắc truy cập theo vai trò (Role-Based Access Parsing Tree): Cấu trúc phân cấp trừu tượng hóa các chú thích an ninh từ các tệp cấu hình Spring Security, phản ánh chính xác cấu trúc logic phân quyền và các điều kiện ràng buộc đi kèm.

Điều kiện biên (Boundary Conditions): Khung phân tích được xác lập chặt chẽ trên các hệ thống phần mềm viết bằng JavaEE, triển khai theo mô hình kiến trúc MVC, tích hợp khung an ninh Spring Security và lưu trữ phân quyền người dùng trong cơ sở dữ liệu quan hệ (SQL).

Phương pháp nghiên cứu tiên tiến

Thiết kế nghiên cứu

Nghiên cứu tuân thủ thế giới quan thực chứng (Positivism) kết hợp phương pháp hình thức (Formal Methods) và suy diễn diễn dịch (Deductive Reasoning). Thiết kế nghiên cứu được cấu trúc thành 3 nhánh tương ứng với 3 bài toán kiểm chứng thực tiễn:

Thành phần thiết kế Nhánh 1: RBAC An ninh lập trình Nhánh 2: RBAC An ninh khai báo Nhánh 3: ABAC Spring Security
Mô hình chính sách RBAC cơ bản (Sandhu et al.) RBAC + SecureUML Constraints ABAC (NIST SP 800-162)
Vị trí mã an ninh Phân tán trong Controller/View XML/Annotations + Database Tệp cấu hình SpEL + Filter
Biểu diễn trung gian Đồ thị khai thác tài nguyên + Ma trận Cây phân tích truy cập vai trò Tập quy tắc vị từ Boolean SpEL
Công cụ hiện thực CheckingRBAC VeRA APVer
Tính chất kiểm chứng Thừa/thiếu quy tắc truy cập Sai lệch phép gán $UA$ và $PA$ Vi phạm tính Bảo mật, Toàn vẹn, Sẵn sàng

Quy trình nghiên cứu rigorous

Quy trình thẩm định mã nguồn được thực hiện qua các bước chuẩn hóa:

  1. Phân tích cú pháp trừu tượng (AST Parsing): Sử dụng các bộ phân tích cú pháp tĩnh để duyệt cây mã nguồn Java, bóc tách toàn bộ các phương thức nghiệp vụ, các tham số HTTP Request và các điểm kiểm tra an ninh (hasPermission, checkPermission).
  2. Trích xuất phân quyền từ cơ sở dữ liệu: Thực thi các truy vấn SQL tự động vào hệ thống cơ sở dữ liệu của ứng dụng để trích xuất tập ánh xạ thực tế $UA \subseteq Users \times Roles$.
  3. Phân tích biểu thức SpEL (Spring Expression Language): Sử dụng engine phân tích ngữ pháp hình thức để chuyển đổi các quy tắc @PreAuthorize và các điều kiện truy cập trong tệp cấu hình thành các mệnh đề logic mệnh đề.
  4. Thực thi thuật toán kiểm chứng hình thức: Đối chiếu cấu trúc phân quyền trích xuất được với ma trận/đặc tả chính sách thiết kế ban đầu.

Data và phân tích

Hệ thống quản lý hồ sơ y tế bệnh viện (Medical Record Management System) được sử dụng làm mẫu kiểm chứng thực nghiệm chuẩn tắc. Mẫu dữ liệu thực nghiệm bao gồm:

  • Tập chủ thể ($S$) và Vai trò ($R$): Bác sĩ ($Doctor$), Y tá ($Nurse$), Lễ tân ($Receptionist$), Bệnh nhân ($Patient$).
  • Tập tài nguyên ($RS$): Hồ sơ bệnh án ($PatientRecords$, $MedicalRecord$), bao gồm các thuộc tính mrID, pID, dID, department, hospital.
  • Tập thao tác ($OP$): $Create$, $Read$, $Update$, $Delete$.
  • Môi trường liên kết đa viện: Bệnh viện A và Bệnh viện B có thỏa thuận chia sẻ hồ sơ bệnh nhân điều trị chéo khoa.

Phát hiện đột phá và implications

Những phát hiện then chốt

Qua quá trình thực nghiệm với 3 công cụ CheckingRBAC, VeRA và APVer trên hệ sinh thái phần mềm quản lý y tế, luận án đã đạt được 4 phát hiện mang tính đột phá:

                            CÁC PHÁT HIỆN ĐỘT PHÁ CỦA NGHIÊN CỨU
[Phát hiện 1: CheckingRBAC] [Phát hiện 2: VeRA]            [Phát hiện 3: APVer]     [Phát hiện 4: Formal Proof]
Định vị lỗi An ninh        Phát hiện xung đột gán         Phát hiện 100% kịch bản   Chứng minh toán học:
Lập trình: Bác sĩ bị gán   quyền CSDL vs. XML:            vi phạm C-I-A trong SpEL:  Thừa quyền -> Mất Bảo mật/
thiếu quyền Update do      Y tá bị cấp sai quyền sửa      Lễ tân đọc bệnh án (C),    Toàn vẹn; Thiếu quyền ->
không đồng bộ View/Servlet. hồ sơ y tế ngoài khoa.        Y tá sửa hồ sơ (I)...      Mất Sẵn sàng.
  1. Phát hiện sự mất đồng bộ nghiêm trọng trong an ninh lập trình (CheckingRBAC): Thuật toán xây dựng ma trận kiểm soát truy cập đã phát hiện trường hợp lập trình viên khai báo quyền trong Controller nhưng bỏ sót liên kết tại giao diện View, dẫn đến việc người dùng có vai trò Bác sĩ bị tước quyền cập nhật hồ sơ y tế một cách không chủ ý.
  2. Vạch trần xung đột giữa cơ sở dữ liệu phân quyền và mã an ninh khai báo (VeRA): Thuật toán kiểm tra phép gán $UA$ và $PA$ đã chỉ ra lỗi phân quyền nghiêm trọng khi cơ sở dữ liệu cấp quyền cho một tài khoản Y tá nhưng cấu hình XML của Spring Security lại không thiết lập ràng buộc sở hữu tài nguyên (Caller.dID), vi phạm nguyên tắc cấp quyền tối thiểu.
  3. Phát hiện chính xác 100% các vi phạm C-I-A trong chính sách ABAC phức tạp (APVer):
    • Vi phạm tính bảo mật (Confidentiality): Phát hiện trường hợp nhân viên Lễ tân được cấp thêm quyền đọc (Read) nội dung chi tiết hồ sơ bệnh án (kịch bản vi phạm rò rỉ dữ liệu).
    • Vi phạm tính toàn vẹn (Integrity): Phát hiện trường hợp Y tá có thêm quyền cập nhật (Update) phác đồ điều trị của Bác sĩ chuyên khoa.
    • Vi phạm tính sẵn sàng (Availability): Phát hiện lỗi lập trình khiến Lễ tân bị mất quyền tạo (Create) hồ sơ y tế cho bệnh nhân mới tại khoa tiếp đón.
  4. Chứng minh toán học về tính toàn vẹn của thuật toán kiểm chứng: Các thuật toán đề xuất đạt độ chính xác tuyệt đối ($Precision = 100%$) trên không gian mẫu thực nghiệm, không phát sinh cảnh báo giả nhờ việc mô hình hóa hình thức chính xác ngữ nghĩa SpEL và cấu trúc bảng quan hệ.

Implications đa chiều

  • Về mặt học thuật (Theoretical Advances): Đóng góp một phương pháp luận hình thức hoàn chỉnh để bắc cầu khoảng trống giữa đặc tả mô hình an ninh mức cao (SecureUML, NIST ABAC) và mã nguồn thực thi mức thấp trong các hệ thống phần mềm hướng thành phần.
  • Về mặt phương pháp luận (Methodological Innovations): Cung cấp quy trình phân tích tĩnh kết hợp CSDL có thể tái sử dụng cho các ngôn ngữ và khung làm việc khác ngoài Java (như .NET Core, Django, Node.js).
  • Về mặt thực tiễn công nghiệp (Industry Applications): Bộ công cụ CheckingRBAC, VeRA và APVer có thể tích hợp trực tiếp vào đường ống DevSecOps (CI/CD Pipeline), tự động chặn đứng các bản build phần mềm chứa lỗi phân quyền trước khi triển khai lên môi trường Production.
  • Về mặt chính sách và tiêu chuẩn (Policy Recommendations): Cung cấp bằng chứng thực nghiệm và công cụ hỗ trợ các tổ chức đạt được các chứng chỉ an ninh thông tin quốc tế khắt khe như ISO/IEC 27001, HIPAA (trong y tế) và PCI-DSS (trong tài chính).

Limitations và Future Research

Mặc dù đạt được những kết quả đột phá, luận án thẳng thắn thừa nhận các giới hạn nghiên cứu:

  1. Phụ thuộc vào công nghệ mục tiêu: Các thuật toán hiện tại được tối ưu hóa riêng cho ngôn ngữ JavaEE, kiến trúc MVC và khung Spring Security; chưa tự động hóa hoàn toàn trên các kiến trúc hiện đại như Microservices, Serverless hoặc GraphQL.
  2. Xử lý mã động và Reflection: Kỹ thuật phân tích tĩnh gặp thách thức cố hữu khi đối mặt với các đoạn mã sử dụng kỹ thuật phản chiếu (Java Reflection), nạp lớp động (Dynamic Class Loading) hoặc các thủ tục lưu trữ phức tạp (Stored Procedures) nằm sâu trong cơ sở dữ liệu.
  3. Giả định về tính đúng đắn của đặc tả: Phương pháp giả định rằng bản đặc tả chính sách an ninh ban đầu luôn nhất quán và không chứa lỗi logic nội tại.

Chương trình nghiên cứu tiếp theo (Future Research Agenda):

  • Mở rộng thuật toán kiểm chứng cho kiến trúc hướng dịch vụ Microservices và môi trường điện toán đám mây phân tán.
  • Tích hợp kỹ thuật phân tích tĩnh với Trí tuệ nhân tạo (LLM-based Code Analysis) để tự động đề xuất các bản vá lỗi mã nguồn (Automated Program Repair).
  • Mở rộng phạm vi kiểm chứng sang các ngôn ngữ lập trình phổ biến khác như Python, Go, Rust và TypeScript.
  • Phát triển module kiểm chứng động lai (Hybrid Static-Dynamic Verification) nhằm xử lý triệt để các lỗ hổng phát sinh từ cơ chế nạp mã động.

Tác động và ảnh hưởng

Nghiên cứu mang lại giá trị tác động sâu rộng trên nhiều bình diện:

  • Tác động học thuật: Định hình chuẩn mực mới trong nghiên cứu Kỹ nghệ phần mềm an toàn tại Việt Nam, mở ra hướng nghiên cứu kết hợp giữa kiểm chứng hình thức và an ninh mã nguồn thực tế với tiềm năng trích dẫn quốc tế cao trên các tạp chí thuộc danh mục ISI/Scopus (Q1/Q2).
  • Chuyển đổi công nghiệp: Giúp các doanh nghiệp phần mềm cắt giảm tới 40-60% chi phí rà soát mã nguồn thủ công (Manual Code Review), loại bỏ nguy cơ bị phạt hàng triệu USD do vi phạm dữ liệu cá nhân theo các nghị định bảo vệ dữ liệu (như GDPR tại Châu Âu hay Nghị định 13/2023/NĐ-CP tại Việt Nam).
  • Lợi ích xã hội: Bảo vệ dữ liệu nhạy cảm của hàng triệu bệnh nhân trong các hệ thống y tế số và bệnh viện thông minh, củng cố niềm tin số của người dân vào các dịch vụ công trực tuyến.

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

  • Nghiên cứu sinh và Giới học thuật: Tiếp cận một khung lý thuyết hoàn chỉnh và các thuật toán hình thức mẫu mực để phát triển các đề tài nghiên cứu chuyên sâu về an ninh phần mềm.
  • Kỹ sư Kỹ nghệ Phần mềm và Chuyên gia DevSecOps: Sở hữu công cụ tự động hóa kiểm tra chính sách an ninh ngay trong quá trình biên dịch mã nguồn, nâng cao chất lượng sản phẩm phần mềm.
  • Giám đốc Công nghệ (CTO) và Giám đốc An ninh thông tin (CISO): Có cơ sở định lượng để đánh giá mức độ tuân thủ chính sách an toàn thông tin của các dự án phần mềm trước khi nghiệm thu.
  • Các Cơ quan Quản lý Nhà nước: Cung cấp công cụ kỹ thuật phục vụ công tác thanh tra, kiểm thử và chứng nhận an toàn thông tin cho các hệ thống thông tin trọng yếu quốc gia.

Câu hỏi chuyên sâu

1. Đóng góp lý thuyết độc đáo nhất của luận án là gì?

Đóng góp độc đáo nhất là việc hình thức hóa toán học quá trình kiểm chứng tĩnh mô hình ABAC chuẩn NIST SP 800-162 trên nền tảng Spring Security. Luận án đã thiết lập các định nghĩa hình thức cho bộ ba tính chất an ninh C-I-A dưới dạng các vị từ logic Boolean trên không gian thuộc tính đa chiều ($S, RS, E, OP$), chuyển hóa một bài toán thẩm định an ninh định tính phức tạp thành bài toán đánh giá logic mệnh đề tự động hóa tuyệt đối.

2. Sự đổi mới về phương pháp luận so với các nghiên cứu quốc tế trước đây?

So với các công cụ kiểm chứng mô hình truyền thống như MOPS (Chen & Wagner, 2002) hay SPlint (Evans & Larochelle, 2002), luận án tạo ra bước đột phá khi kết hợp đồng thời ba nguồn thông tin: Cây cú pháp trừu tượng (AST) của mã nguồn Controller/View, Cây phân tích cú pháp biểu thức an ninh (SpEL) và Cấu trúc quan hệ thực tế trong Cơ sở dữ liệu ($UA/PA$). Điều này giúp loại bỏ điểm nghẽn phải viết chú thích thủ công và bao phủ trọn vẹn cả hai phương thức an ninh lập trình lẫn an ninh khai báo.

3. Phát hiện thực nghiệm bất ngờ nhất từ dữ liệu là gì?

Phát hiện bất ngờ nhất là sự tồn tại phổ biến của các lỗi vi phạm tính sẵn sàng (Availability) trong các ứng dụng Spring Security. Trong khi cộng đồng an ninh thường chỉ tập trung vào lỗi lộ lọt dữ liệu (Confidentiality) hoặc sửa đổi trái phép (Integrity), công cụ APVer đã chứng minh rằng các sai sót cú pháp nhỏ trong việc định nghĩa biểu thức SpEL có thể tước bỏ hoàn toàn quyền truy cập hợp pháp của người dùng nghiệp vụ (như Lễ tân không thể tạo bệnh án mới), làm tê liệt quy trình vận hành thực tế của tổ chức.

4. Luận án có cung cấp quy trình tái lập (Replication Protocol) không?

Có. Luận án mô tả chi tiết kiến trúc thuật toán, mã giả (Pseudocode) của toàn bộ 7 thuật toán cốt lõi, cấu trúc siêu dữ liệu XML, định dạng tệp đặc tả chính sách và cung cấp đầy đủ các kịch bản thực nghiệm trên hệ thống quản lý hồ sơ y tế bệnh viện với các tệp mã nguồn mẫu trong các chương 3, 4 và 5.

5. Kế hoạch nghiên cứu 10 năm tới được phác thảo như thế nào?

Lộ trình 10 năm tập trung vào 3 trụ cột: (i) Mở rộng lý thuyết kiểm chứng an ninh cho mô hình Zero Trust Architecture và Microservices Mesh; (ii) Xây dựng công cụ kiểm chứng tự động đa ngôn ngữ hỗ trợ Cloud-Native; (iii) Tích hợp học sâu và mô hình ngôn ngữ lớn để tự động hóa toàn diện chu trình "Phát hiện lỗi – Kiểm chứng mô hình – Tự động sinh mã sửa lỗi" (Self-Healing Software Security).

Kết luận

Luận án tiến sĩ của NCS. Lương Thanh Nhạn đã hoàn thành xuất sắc các mục tiêu nghiên cứu đề ra với 5 đóng góp cốt lõi:

  1. Xây dựng phương pháp và thuật toán kiểm chứng chính sách RBAC triển khai bằng an ninh lập trình thông qua Đồ thị khai thác tài nguyên và Ma trận kiểm soát truy cập.
  2. Xây dựng phương pháp và thuật toán kiểm chứng chính sách RBAC kết hợp ràng buộc cấp quyền (SecureUML) trong an ninh khai báo thông qua Cây phân tích truy cập và phân tích CSDL quan hệ.
  3. Xây dựng khung lý thuyết hình thức và thuật toán kiểm chứng chính sách ABAC triển khai qua Spring Security/SpEL đối với bộ ba tính chất an ninh C-I-A.
  4. Phát triển thành công 3 công cụ phần mềm hoàn chỉnh: CheckingRBAC, VeRA và APVer với giao diện đồ họa trực quan và độ chính xác kiểm chứng tuyệt đối.
  5. Thực nghiệm kiểm chứng thành công trên hệ thống quản lý hồ sơ y tế, chứng minh tính khả thi và hiệu quả kinh tế – kỹ thuật vượt trội của phương pháp đề xuất.

Công trình tạo tiền đề vững chắc cho việc nâng cao chất lượng và độ tin cậy an ninh của các hệ thống phần mềm quy mô lớn, đóng góp thiết thực cho sự phát triển của ngành Kỹ nghệ phần mềm và an toàn thông tin tại Việt Nam và quốc tế.