Luận án TS Lương Thanh Nhạn: Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm web Java

ĐẠ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 LUẬN ÁN TIẾN SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - 20 ĐẠ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 Chuyên ngành: Kỹ thuật phần mềm Mã số: 9480103.01 LUẬN ÁN TIẾN SĨ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS. Trương Ninh Thuận Hà Nội - 20 Lời cam đoan Tôi xin cam đoan luận án “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” là công trình nghiên cứu của riêng tôi. Các số liệu, kết quả được trình bày trong luận án là hoàn toàn trung thực và chưa từng được công bố trong bất kỳ một công trình nào khác.  Tôi đã trích dẫn đầy đủ các tài liệu tham khảo, công trình nghiên cứu liên quan ở trong nước và quốc tế.

Ngoại trừ các tài liệu tham khảo này, luận án hoàn toàn là công việc của riêng tôi.  Trong các công trình khoa học được công bố trong luận án, tôi đã thể hiện rõ ràng và chính xác đóng góp của các đồng tác giả và những gì do tôi đã đóng góp.  Luận án được hoàn thành trong thời gian tôi làm Nghiên cứu sinh tại Bộ môn Công nghệ phần mềm, Khoa Công nghệ Thông tin, Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội. Tác giả: Hà Nội: i Lời cảm ơn Trước hết, tôi muốn bày tỏ sự biết ơn đến PGS.

Trương Ninh Thuận, cán bộ hướng dẫn, người đã trực tiếp giảng dạy và định hướng tôi trong suốt thời gian học cao học, thực hiện luận văn thạc sĩ cũng như luận án này. Thầy đã hướng dẫn cho tôi nhiều kiến thức trong học thuật và nghiên cứu. Một vinh dự lớn cho tôi khi được học tập, nghiên cứu dưới sự hướng dẫn của Thầy. Tôi xin bày tỏ sự biết ơn sâu sắc đến các Thầy, Cô trong Bộ môn Công nghệ phần mềm vì sự tận tâm, giúp đỡ của các Thầy Cô và các đóng góp rất hữu ích cho luận án.

Tôi xin trân trọng cảm ơn Khoa Công nghệ thông tin, Phòng Đào tạo và Ban Giám hiệu trường Đại học Công nghệ đã tạo điều kiện thuận lợi cho tôi trong suốt quá trình học tập và nghiên cứu tại Trường. Tôi cũng bày tỏ sự biết ơn đến Ban Giám hiệu, các Phòng, Ban, Bộ môn liên quan trong Trường Đại học Y Dược Hải Phòng đã tạo điều kiện về thời gian và tài chính cho tôi thực hiện luận án này. Tôi muốn cảm ơn đến các đồng nghiệp trong Bộ môn Tin học, Trường Đại học Y Dược Hải Phòng đã giúp đỡ, động viên và sát cánh bên tôi trong suốt quá trình nghiên cứu. Tôi muốn cảm ơn đến tất cả những người bạn của tôi, các anh/chị/em nghiên cứu sinh - những người luôn chia sẻ, động viên tôi bất cứ khi nào tôi cần và tôi luôn ghi nhớ những điều đó.

Cuối cùng, tôi xin bày tỏ lòng biết ơn vô hạn đối với cha, mẹ, chồng, con đã luôn ủng hộ và yêu thương tôi vô điều kiện. Nếu không có sự ủng hộ của gia đình tôi không thể hoàn thành được luận án này. Lương Thanh Nhạn ii Tóm tắt Các hệ thống phần mềm hiện được sử dụng sâu rộng trong hầu hết mọi lĩnh vực. Bên cạnh những lợi ích mà phần mềm mang lại cho con người thì các vấn đề vi phạm an ninh phần mềm cũng xuất hiện ngày càng đa dạng và phức tạp, đặc biệt là với các hệ thống web.

Trong thực tế, điều khiển truy cập là một trong những biện pháp hiệu quả để thực thi chính sách an ninh của các hệ thống phần mềm nhằm 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 của các hệ thống ứng dụng luôn tiềm ẩn các lỗi, nhất là ở giai đoạn lập trình. Nếu những lỗi này được phát hiện càng muộn thì chi phí sửa chữa hệ thống càng lớn và hậu quả càng phức tạp. Đây cũng là vấn đề luôn được quan tâm bởi cả cộng đồng phát triển phần mềm.

Chính vì thế, trong quá trình xây dựng và phát triển phần mềm, việc kiểm chứng từ mã nguồn của ứng dụng để đảm bảo chính sách điều khiển truy cập được triển khai chính xác ở giai đoạn lập trình sẽ mang lại hiệu quả kinh tế và gia tăng chất lượng của phần mềm. Dựa trên nền tảng của kỹ thuật phân tích tĩnh, luận án đề xuất một số phương pháp kiểm chứng chính sách điều khiển truy cập của các hệ thống web. Cụ thể, các hệ thống web mà luận án hướng đến phân tích đều được xây dựng bởi ngôn ngữ lập trình Java theo kiến trúc MVC (Model-View-Controller) và có chính sách điều khiển truy cập theo vai trò hoặc chính sách điều khiển truy cập theo thuộc tính được triển khai theo phương pháp an ninh lập trình, an ninh khai báo. Các đóng góp chính của luận án bao gồm: (i) Đề xuất phương pháp kiểm chứng chính sách điều khiển truy cập theo vai trò triển khai theo phương pháp an ninh lập trình.

Chính sách điều khiển truy cập theo vai trò của ứng dụng web được trích rút thông qua việc 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 và đồ thị khai thác tài nguyên. Một 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 các quy tắc truy cập của hệ thống web. Từ đó, luận án đề xuất 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ả. Bên cạnh đó, một công cụ tên là CheckingRBAC được xây dựng để hỗ trợ quá trình kiểm chứng theo phương pháp đã đề xuất.

iii (ii) Đề xuất phương pháp kiểm chứng chính sách điều khiển truy cập theo vai trò 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à các ràng buộc cấp quyền của các hệ thống web được kiểm tra thông qua phép gán vai trò - người dùng và phép gán vai trò - quyền. Với phép gán thứ nhất, 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. Ở phép gán thứ hai, 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ò.

Sau đó, các thuật toán được đề xuất để kiểm tra tính chính xác của các phép gán đã triển khai trong các hệ thống web. 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. (iii) Đề 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. Đầu tiên, tiến trình kiểm chứng được thực hiện bằng việc 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.

Tiếp theo, sự phù hợp giữa chính sách điều khiển truy cập của ứng dụng và đặc tả được tiến hành thông qua các định nghĩa hình thức và các thuật toán 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. Cuối cùng, 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. Ngoài ra, các công cụ phát triển từ các phương pháp đề xuất cũng đã được tiến hành thực nghiệm với hệ thống quản lý hồ sơ y tế. Bước đầu, phương pháp và công cụ đề xuất đã cho các kết quả kiểm chứng chính xác như dự kiến.

Từ khóa: kiểm chứng, điều khiển truy cập, RBAC, ABAC, an ninh phần mềm, phân tích tĩnh. iv Mục lục Lời cam đoan. iii Mục lục. iv Danh mục các từ viết tắt.

viii Danh mục các hình vẽ. ix Danh mục các thuật toán. xi Danh mục các đặc tả. xii Chương 1.

Nội dung nghiên cứu. Đóng góp của luận án. Cấu trúc luận án. KIẾN THỨC CƠ SỞ.

An ninh phần mềm. Một số tính chất an ninh của phần mềm. Chính sách điều khiển truy cập. Một số mô hình chính sách điều khiển truy cập.

Điều khiển truy cập theo vai trò. Ngôn ngữ mô hình hóa chính sách an ninh thống nhất. Điều khiển truy cập theo thuộc tính. Triển khai chính sách điều khiển truy cập trong JavaEE.

An ninh truy cập trong JavaEE. Một số kiến trúc thiết kế phần mềm trong JavaEE. Phân tích và biểu diễn chương trình. Phân tích chương trình.

Một số phương pháp biểu diễn chương trình. Tóm tắt chương. KIỂM CHỨNG CHÍNH SÁCH RBAC TRIỂN KHAI THEO PHƯƠNG PHÁP AN NINH LẬP TRÌNH. Các nghiên cứu liên quan.

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. Tập quy tắc truy cập đặc tả. Danh sách các quyền. Đồ thị khai thác tài nguyên.

Ma trận kiểm soát truy cập theo vai trò. 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ả. Công cụ kiểm chứng. Giao diện công cụ.

Thảo luận và đánh giá. Tóm tắt chương. 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. Các nghiên cứu liên quan.

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. Kiểm tra phép gán người dùng - vai trò. Kiểm tra phép gán vai trò - quyền. Công cụ kiểm chứng.

Kiến trúc của công cụ. Giao diện đồ họa của công cụ. Thảo luận và đánh giá. Tóm tắt chương.

83 vi Chương 5. KIỂM CHỨNG CHÍNH SÁCH ĐIỀU KHIỂN TRUY CẬP THEO THUỘC TÍNH. Các nghiên cứu liên quan. Phương pháp kiểm chứng chính sách điều khiển truy cập theo thuộc tính.

Chính sách ABAC đặc tả của hệ thống. Chính sách ABAC triển khai trong ứng dụng. Các thuật toán kiểm chứng chính sách ABAC. Công cụ kiểm chứng.

Xây dựng công cụ. Thảo luận và đánh giá. Tóm tắt chương. Hướng phát triển.

111 Danh mục các công trình khoa học. 113 Tài liệu tham khảo .