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.
