Kiểm chứng chính sách điều khiển truy cập cho hệ thống phần mềm: Luận án Tiến sĩ

LỜI CAM ĐOAN

LỜI CẢM ƠN

TÓM TẮT

1. CHƯƠNG 1: NỘI DUNG NGHIÊN CỨU

1.1. Đóng góp của luận án

1.2. Cấu trúc luận án

1.3. KIẾN THỨC CƠ SỞ

1.3.1. An ninh phần mềm

1.3.2. Một số tính chất an ninh của phần mềm

1.3.3. Chính sách điều khiển truy cập

1.3.4. Một số mô hình chính sách điều khiển truy cập

1.3.5. Điều khiển truy cập theo vai trò

1.3.6. Ngôn ngữ mô hình hóa chính sách an ninh thống nhất

1.3.7. Điều khiển truy cập theo thuộc tính

1.3.8. Triển khai chính sách điều khiển truy cập trong JavaEE

1.3.9. An ninh truy cập trong JavaEE

1.3.10. Một số kiến trúc thiết kế phần mềm trong JavaEE

1.3.11. Phân tích và biểu diễn chương trình

1.3.11.1. Phân tích chương trình

1.3.11.2. Một số phương pháp biểu diễn chương trình

1.3.12. Tóm tắt chương

2. KIỂM CHỨNG CHÍNH SÁCH RBAC TRIỂN KHAI THEO PHƯƠNG PHÁP AN NINH LẬP TRÌNH

2.1. Các nghiên cứu liên quan

2.2. Phương pháp kiểm chứng chính sách RBAC triển khai theo phương pháp an ninh lập trình

2.2.1. Tập quy tắc truy cập đặc tả

2.2.2. Danh sách các quyền

2.2.3. Đồ thị khai thác tài nguyên

2.2.4. Ma trận kiểm soát truy cập theo vai trò

2.2.5. Thuật toán kiểm tra sự phù hợp của ma trận kiểm soát truy cập theo vai trò và chính sách RBAC đã đặc tả

2.2.6. Công cụ kiểm chứng

2.2.6.1. Giao diện công cụ

2.2.7. Thảo luận và đánh giá

2.2.8. Tóm tắt chương

3. KIỂM CHỨNG CHÍNH SÁCH RBAC KẾT HỢP RÀNG BUỘC CẤP QUYỀN TRIỂN KHAI THEO PHƯƠNG PHÁP AN NINH KHAI BÁO

3.1. Các nghiên cứu liên quan

3.2. Phương pháp kiểm chứng chính sách RBAC kết hợp ràng buộc cấp quyền triển khai theo phương pháp an ninh khai báo

3.2.1. Kiểm tra phép gán người dùng - vai trò

3.2.2. Kiểm tra phép gán vai trò - quyền

3.2.3. Công cụ kiểm chứng

3.2.3.1. Kiến trúc của công cụ

3.2.3.2. Giao diện đồ họa của công cụ

3.2.4. Thảo luận và đánh giá

3.2.5. Tóm tắt chương

4. KIỂM CHỨNG CHÍNH SÁCH ĐIỀU KHIỂN TRUY CẬP THEO THUỘC TÍNH

4.1. Các nghiên cứu liên quan

4.2. Phương pháp kiểm chứng chính sách điều khiển truy cập theo thuộc tính

4.2.1. Chính sách ABAC đặc tả của hệ thống

4.2.2. Chính sách ABAC triển khai trong ứng dụng

4.2.3. Các thuật toán kiểm chứng chính sách ABAC

4.2.4. Công cụ kiểm chứng

4.2.4.1. Xây dựng công cụ

4.2.5. Thảo luận và đánh giá

4.2.6. Tóm tắt chương

4.3. Hướng phát triển

DANH MỤC CÁC CÔNG TRÌNH KHOA HỌC

TÀI LIỆU THAM KHẢO

I. Tổng Quan Vì Sao Cần Kiểm Chứng Chính Sách Truy Cập

Các hệ thống phần mềm ngày càng được sử dụng rộng rãi, tiềm ẩn nhiều nguy cơ bảo mật. Điều khiển truy cập là một biện pháp hiệu quả để thực thi chính sách an ninh, ngăn chặn các vi phạm truy cập. Tuy nhiên, quá trình triển khai chính sách điều khiển truy cập thường tiềm ẩn lỗi, đặc biệt trong giai đoạn lập trình. Việc phát hiện lỗi muộn sẽ tốn kém chi phí sửa chữa và gây ra hậu quả nghiêm trọng. Vì vậy, kiểm chứng từ mã nguồn ứng dụng là rất quan trọng để đảm bảo chính sách điều khiển truy cập được triển khai chính xác, mang lại hiệu quả kinh tế và nâng cao chất lượng phần mềm. Luận án này tập trung vào việc đề xuất các phương pháp kiểm chứng chính sách điều khiển truy cập cho các hệ thống web dựa trên kỹ thuật phân tích tĩnh, giúp phát hiện sớm các lỗ hổng bảo mật.

1.1. An Ninh Phần Mềm Nguy Cơ Tiềm Ẩn Trong Hệ Thống Web

Hệ thống web hiện nay đối mặt với nhiều nguy cơ bảo mật và khai thác tài nguyên trái phép. Các biện pháp bảo vệ chia thành 3 nhóm: xây dựng ứng dụng an toàn, áp dụng biện pháp bảo vệ (proxy), và thiết lập thành phần cơ sở hạ tầng để giám sát. Để bảo vệ tài nguyên, chính sách an ninh là cần thiết, bao gồm mã hóa, điều khiển truy cập và truyền thông an toàn.

1.2. Điều Khiển Truy Cập Biện Pháp Đảm Bảo An Toàn và Bảo Mật

Điều khiển truy cập là biện pháp quan trọng để đảm bảo tính bảo mật, toàn vẹn và sẵn sàng của hệ thống phần mềm. Tuy nhiên, việc triển khai chính sách điều khiển truy cập luôn tiềm ẩn lỗ hổng an ninh, do không tuân thủ hoặc bỏ sót yêu cầu an ninh. Lỗi lập trình, hiểu sai yêu cầu đặc tả cũng là nguyên nhân. Phần mềm càng lớn, việc triển khai càng phức tạp và dễ sai sót.

II. Thách Thức và Hướng Tiếp Cận trong Kiểm Chứng Truy Cập

Bài toán kiểm chứng chính sách điều khiển truy cập là một nhiệm vụ quan trọng giúp phát hiện sớm sai sót và đảm bảo tính an ninh phần mềm. Các nghiên cứu hiện tại tiếp cận theo nhiều hướng, từ xây dựng mô hình, đặc tả tính chất an ninh, đến phân tích và thẩm định chính sách điều khiển truy cập ở nhiều giai đoạn phát triển. Một số phương pháp còn xây dựng công cụ để tự động phát hiện lỗ hổng bảo mật từ mã nguồn. Luận án này tập trung vào các hệ thống web xây dựng bằng Java, theo kiến trúc MVC và áp dụng chính sách điều khiển truy cập theo vai trò hoặc thuộc tính.

2.1. Phân Tích Tĩnh Nền Tảng của Phương Pháp Kiểm Chứng

Luận án đề xuất các phương pháp kiểm chứng dựa trên nền tảng của kỹ thuật phân tích tĩnh. Phân tích tĩnh kiểm tra mã nguồn mà không cần thực thi, giúp xác định các lỗ hổng tiềm ẩn. Tuy nhiên, phương pháp này có thể đưa ra cảnh báo sai. Phân tích động, ngược lại, đảm bảo tính đúng đắn của lỗ hổng được xác định, nhưng không thể đảm bảo tính đầy đủ.

2.2. Kiểm Chứng RBAC và ABAC Hai Hướng Nghiên Cứu Chính

Luận án tập trung vào hai mô hình điều khiển truy cập: Kiểm soát truy cập dựa trên vai trò (RBAC) và Kiểm soát truy cập dựa trên thuộc tính (ABAC). Các nghiên cứu về RBAC chủ yếu kiểm tra phép gán giữa quyền và vai trò. Với ABAC, một số nghiên cứu tập trung vào đặc tả, triển khai và kiểm thử chính sách điều khiển truy cập với Spring Security, nhưng chưa xác minh tính bảo mật chỉ bằng phân tích mã nguồn.

2.3. Mục tiêu chung của luận án bao gồm

(i) Xây dựng các phương pháp phân tích, biểu diễn chính sách điều khiển truy cập từ mã nguồn của các hệ thống web và các thuật toán kiểm tra sự phù hợp của mô hình biểu diễn chính sách so với...'

III. Kiểm Chứng Chính Sách RBAC An Ninh Lập Trình Giải Pháp

Luận án đề xuất phương pháp kiểm chứng chính sách điều khiển truy cập theo vai trò (RBAC) triển khai theo phương pháp an ninh lập trình. Chính sách RBAC của ứng dụng web được trích rút thông qua phân tích phương thức khai thác tài nguyên, xây dựng danh sách quyền và đồ thị khai thác tài nguyên. Ma trận kiểm soát truy cập tài nguyên theo vai trò được giới thiệu để biểu diễn quy tắc truy cập. Thuật toán kiểm tra sự phù hợp giữa ma trận kiểm soát và chính sách truy cập đã đặc tả được đề xuất. Công cụ CheckingRBAC được xây dựng để hỗ trợ.

3.1. Trích rút các quyền truy cập từ mã

Phân tích các phương thức khai thác tài nguyên, xây dựng danh sách các quyền.

3.2. Xây dựng ma trận kiểm soát truy cập

Xây dựng ma trận kiểm soát truy cập tài nguyên theo vai trò. Ma trận này biểu diễn các quy tắc truy cập của hệ thống web. Thuật toán kiểm tra sự phù hợp giữa ma trận kiểm soát truy cập theo vai trò và chính sách truy cập đã đặc tả.

3.3. CheckingRBAC Tool

Xây dựng công cụ CheckingRBAC để hỗ trợ quá trình kiểm chứng theo phương pháp đã đề xuất.

IV. RBAC và Ràng Buộc Kiểm Chứng An Ninh Khai Báo Chi Tiết

Luận án đề xuất phương pháp kiểm chứng chính sách điều khiển truy cập RBAC kết hợp ràng buộc cấp quyền triển khai theo phương pháp an ninh khai báo. Chính sách điều khiển truy cập và ràng buộc cấp quyền được kiểm tra thông qua phép gán vai trò - người dùng và vai trò - quyền. Phép gán thứ nhất dựa trên phân tích cơ sở dữ liệu. Với phép gán thứ hai, quy tắc truy cập được phân tích và biểu diễn thành cây phân tích quy tắc truy cập. Thuật toán kiểm tra tính chính xác của phép gán đã triển khai được đề xuất. Công cụ VeRA được xây dựng.

4.1. Kiểm tra phép gán user role

Phương pháp được tiến hành dựa trên việc phân tích cơ sở dữ liệu của hệ thống ứng dụng

4.2.Kiểm tra phép gán role permission

Các quy tắc truy cập của hệ thống web được phân tích và biểu diễn thành cây phân tích quy tắc truy cập tài nguyên theo vai trò.

4.3. VeRA Tool

Phương pháp đề xuất đã được triển khai thành công cụ VeRA để kiểm chứng tự động các hệ thống web.

V. Kiểm Chứng ABAC Giải Pháp Cho Hệ Thống An Toàn

Luận án đề xuất phương pháp kiểm chứng chính sách điều khiển truy cập theo thuộc tính (ABAC). Tiến trình kiểm chứng thực hiện bằng cách trích rút và phân tích quy tắc truy cập trong hệ thống web. Sự phù hợp giữa chính sách điều khiển truy cập và đặc tả được tiến hành thông qua định nghĩa hình thức và thuật toán kiểm tra tính bảo mật, toàn vẹn và sẵn sàng. Công cụ kiểm chứng APVer đã được phát triển.

5.1. Phân tích quy tắc truy cập

Trích rút, phân tích các quy tắc truy cập được triển khai trong hệ thống web.

5.2. Xác minh và bảo đảm ABAC

Kiểm tra tính bảo mật, tính toàn vẹn và tính sẵn sàng chính sách truy cập của hệ thống.

5.3. APVer Tool

Công cụ kiểm chứng APVer đã được phát triển từ phương pháp đề xuất để thực hiện quá trình kiểm chứng tự động.

VI. Kết Luận và Hướng Phát Triển Kiểm Chứng Chính Sách

Luận án đã đề xuất các phương pháp kiểm chứng chính sách điều khiển truy cập hiệu quả cho hệ thống phần mềm. Các công cụ CheckingRBAC, VeRA và APVer đã được xây dựng và thử nghiệm thành công. Hướng phát triển tiếp theo có thể tập trung vào việc mở rộng phạm vi áp dụng cho các loại hình hệ thống phần mềm khác, cải thiện hiệu suất của thuật toán kiểm chứng, và tích hợp các công cụ vào quy trình phát triển phần mềm.

6.1. Mở Rộng Phạm Vi Ứng Dụng

Mở rộng phạm vi áp dụng cho các loại hình hệ thống phần mềm khác.

6.2. Cải Thiện Hiệu Suất

Cải thiện hiệu suất của thuật toán kiểm chứng.

6.3. Tích Hợp Quy Trình

Tích hợp các công cụ vào quy trình phát triển phần mềm.

ĐẠI HỌC 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