Luận án Tiến sĩ Công nghệ thông tin: 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

Chia sẻ: _ _ | Ngày: | Loại File: PDF | Số trang:137

Thêm vào BST

Báo xấu

22
lượt xem 5
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Nội dung chính của luận án tập trung nghiên cứu các mô hình biểu diễn các chính sách điều khiển truy cập của hệ thống phần mềm: đ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 (SecureUML), điều khiển truy cập theo thuộc tính. Mời các bạn tham khảo!

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Luận án Tiến sĩ Công nghệ thông tin: 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

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ LƯƠNG THANH NHẠ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 LUẬN ÁN TIẾN SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - 2021
ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ LƯƠNG THANH NHẠ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 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.TS. Trương Ninh Thuận Hà Nội - 2021
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.TS. 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. NCS. 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . i Lời cảm ơn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ii Tóm tắt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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. GIỚI THIỆU. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1. Đặt vấn đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2. Nội dung nghiên cứu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3. Đóng góp của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.4. Cấu trúc luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Chương 2. KIẾN THỨC CƠ SỞ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1. An ninh phần mềm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1.1. Một số tính chất an ninh của phần mềm . . . . . . . . . . . . . . . . . . . . . . . 10 2.1.2. Chính sách điều khiển truy cập . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2. Một số mô hình chính sách điều khiển truy cập . . . . . . . . . . . . . . . . . . . . 14 2.2.1. Điều khiển truy cập theo vai trò . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.2. Ngôn ngữ mô hình hóa chính sách an ninh thống nhất . . . . . . . . . 17 2.2.3. Điều khiển truy cập theo thuộc tính . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.3. Triển khai chính sách điều khiển truy cập trong JavaEE . . . . . . . . . . . 23 2.3.1. An ninh truy cập trong JavaEE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.3.2. Một số kiến trúc thiết kế phần mềm trong JavaEE . . . . . . . . . . . . . 24 2.4. Phân tích và biểu diễn chương trình . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.4.1. Phân tích chương trình . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.4.2. Một số phương pháp biểu diễn chương trình . . . . . . . . . . . . . . . . . . . 34 2.5. Tóm tắt chương . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 v
Chương 3. KIỂM CHỨNG CHÍNH SÁCH RBAC TRIỂN KHAI THEO PHƯƠNG PHÁP AN NINH LẬP TRÌNH . . . . . . . . . . . . . 39 3.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 3.3. 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. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.3.1. Tập quy tắc truy cập đặc tả . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.3.2. Danh sách các quyền . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.3.3. Đồ thị khai thác tài nguyên . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.3.4. Ma trận kiểm soát truy cập theo vai trò . . . . . . . . . . . . . . . . . . . . . . . 49 3.3.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ả . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 3.4. Công cụ kiểm chứng . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 3.4.1. Giao diện công cụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 3.4.2. Thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 3.5. Thảo luận và đánh giá . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 3.6. Tóm tắt chương . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 Chương 4. 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 4.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 4.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 4.3. 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 . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.3.1. Kiểm tra phép gán người dùng - vai trò . . . . . . . . . . . . . . . . . . . . . . . . 68 4.3.2. Kiểm tra phép gán vai trò - quyền . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 4.4. Công cụ kiểm chứng . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 4.4.1. Kiến trúc của công cụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 4.4.2. Giao diện đồ họa của công cụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.4.3. Thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 4.5. Thảo luận và đánh giá . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 4.6. 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 5.3. Phương pháp kiểm chứng chính sách điều khiển truy cập theo thuộc tính. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.3.1. Chính sách ABAC đặc tả của hệ thống . . . . . . . . . . . . . . . . . . . . . . . . 90 5.3.2. Chính sách ABAC triển khai trong ứng dụng . . . . . . . . . . . . . . . . . . 91 5.3.3. Các thuật toán kiểm chứng chính sách ABAC . . . . . . . . . . . . . . . . . . 92 5.4. Công cụ kiểm chứng . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 5.4.1. Xây dựng công cụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 5.4.2. Thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98 5.5. Thảo luận và đánh giá . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 5.6. Tóm tắt chương . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 Chương 6. KẾT LUẬN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 6.1. Kết luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 6.2. 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 vii
Danh mục các từ viết tắt Từ viết Từ gốc Giải nghĩa - Tạm dịch tắt ABAC Attribute-Based Access Điều khiển truy cập dựa trên thuộc Control tính API Application Programming Giao diện lập trình ứng dụng Interface AST Abstract Syntax Tree Cây cú pháp trừu tượng CFG Control Flow Graph Đồ thị luồng điều khiển DAC Discretionary Access Con- Điều khiển truy cập tùy ý trol FSA Finite State Automata Ôtômat hữu hạn trạng thái HTML Hypertext Markup Lan- Ngôn ngữ đánh dấu siêu văn bản guage IEC International Electrotechni- Uỷ ban kỹ thuật điện quốc tế cal Commission ISO International Organization Tổ chức tiêu chuẩn hoá quốc tế for Standardization MAC Mandatory Access Control Điều khiển truy cập bắt buộc MVC Model-View-Controller Mô hình-Khung nhìn-Bộ điều khiển NIST National Institute of Stan- Viện Tiêu chuẩn và Kĩ thuật Quốc dards and Technology gia Mỹ PDA Push Down Automaton Ôtômat đẩy xuống PDP Policy Decision Point Điểm quyết định chính sác PEP Policy Enforcement Point Điểm thực thi chính sách PDG Program Dependence Graph Đồ thị phụ thuộc chương trình PHP Hypertext Preprocessor Mộ xử lý siêu văn bản - một ngôn ngữ lập trình kịch bản RBAC Role-Based Access Control Điều khiển truy cập dựa trên vai trò OASIS Organization for the Ad- Tổ chức cải tiến các tiêu chuẩn vancement of Structured In- thông tin có cấu trúc formation Standards viii
SDG System Dependence Graph Đồ thị phụ thuộc hệ thống SoD Separation of Duties Phân chia nhiệm vụ SpEL Spring Expression Language Ngôn ngữ biểu thức Spring SQL Structured Query Language Ngôn ngữ truy vấn có cấu trúc SSL Secure Sockets Layer Lớp socket bảo mật TLS Transport Layer Security Bảo mật tầng giao vận UML Unified Modeling Language Ngôn ngữ mô hình hóa thống nhất URL Uniform Resource Locator Định vị tài nguyên thống nhất XACML eXtensible Access Control Ngôn ngữ đánh dấu kiểm soát truy Markup Language cập mở rộng XML Extensible Markup Lan- Ngôn ngữ đánh dấu mở rộng guage ix
Danh mục các hình vẽ 1.1 Cấu trúc của luận án. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.1 Một số tính chất an ninh của phần mềm. . . . . . . . . . . . . . . . . 11 2.2 Điều khiển truy cập và một số dịch vụ an ninh. . . . . . . . . . . . . . 13 2.3 Mô hình RBAC cơ bản. . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.4 Siêu mô hình SecureUML. . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.5 Chính sách điều khiển truy cập của hệ thống quản lý hồ sơ y tế bằng SecureUML. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.6 Cơ chế điều khiển truy cập theo thuộc tính. . . . . . . . . . . . . . . . 20 2.7 Kiến trúc MVC trong JavaEE. . . . . . . . . . . . . . . . . . . . . . . 25 2.8 Kiến trúc tổng quát của Spring Security. . . . . . . . . . . . . . . . . . 27 2.9 Kiến trúc Spring triển khai ABAC trong JavaEE. . . . . . . . . . . . 27 2.10 Các hoạt động đảm bảo chính sách an ninh phần mềm. . . . . . . . . 29 2.11 Cây cú pháp trừu tượng biểu diễn đoạn mã của giải thuật tìm ước số chung lớn nhất. . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.12 Minh họa đồ thị gọi một chương trình phần mềm. . . . . . . . . . . . 37 2.13 Một số ví dụ đồ thị luồng điều khiển. . . . . . . . . . . . . . . . . . . . 37 2.14 Đồ thị luồng điều khiển mô tả mức độ chi tiết của chương trình con. 38 3.1 Quy trình kiểm chứng chính sách RBAC triển khai theo phương pháp an ninh lập trình. . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 3.2 Giao diện của công cụ kiểm chứng chính sách RBAC. . . . . . . . . . 55 3.3 Mô hình triển khai chính sách RBAC trong hệ thống quản lý hồ sơ y tế. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 3.4 Đồ thị khai thác tài nguyên của hệ thống quản lý hồ sơ y tế. . . . . . 59 3.5 Ma trận kiểm soát truy cập theo vai trò của hệ thống quản lý hồ sơ y tế. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 4.1 Quy trình 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. . . . . . . . . . 68 4.2 Cấu trúc cây phân tích truy cập theo vai trò. . . . . . . . . . . . . . . 71 4.3 Tiến trình xây dựng cây phân tích truy cập theo vai trò của các ứng dụng web. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 x
4.4 Kiến trúc của công cụ kiểm chứng chính sách RBAC kết hợp ràng buộc cấp quyền. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.5 Giao diện của công cụ kiểm chứng chính sách RBAC kết hợp ràng buộc cấp quyền. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.6 Cơ sở dữ liệu của phép gán vai trò - người dùng. . . . . . . . . . . . . 79 4.7 Cây phân tích truy cập theo vai trò của hệ thống quản lý hồ sơ y tế. 80 5.1 Quy trình kiểm chứng chính sách điều khiển truy cập theo thuộc tính.90 5.2 Giao diện đồ họa của công cụ APVer. . . . . . . . . . . . . . . . . . . 98 5.3 Kết quả kiểm chứng tính bảo mật khi lễ tân có thêm quyền đọc hồ sơ y tế. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 5.4 Kết quả kiểm chứng tính toàn vẹn khi y tá có thêm quyền cập nhật hồ sơ y tế. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 5.5 Kết quả kiểm chứng tính sẵn sàng khi lễ tân thiếu quyền tạo hồ sơ y tế. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 xi
Danh mục các thuật toán 3.1 Xây dựng ma trận kiểm soát truy cập theo vai trò. . . . . . . . . . . . 51 3.2 Kiểm tra ma trận kiểm soát truy cập theo vai trò và chính sách RBAC đã đặc tả. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 4.1 Kiểm tra phép gán người dùng - vai trò . . . . . . . . . . . . . . . . . 69 4.2 Kiểm tra phép gán vai trò - quyền . . . . . . . . . . . . . . . . . . . . 75 5.1 Kiểm tra tính bảo mật chính sách truy cập. . . . . . . . . . . . . . . . 94 5.2 Kiểm tra tính toàn vẹn chính sách truy cập. . . . . . . . . . . . . . . . 96 5.3 Kiểm tra tính sẵn sàng chính sách truy cập. . . . . . . . . . . . . . . . 97 xii
Danh mục các đặc tả 2.1 Mã nguồn của hàm hasPermission . . . . . . . . . . . . . . . . . . . . 27 2.2 Mã nguồn của hàm checkPermission . . . . . . . . . . . . . . . . . . . 28 3.1 Cấu trúc tệp đặc tả chính sách RBAC của hệ thống . . . . . . . . . . 45 3.2 Đặc tả chính sách RBAC của hệ thống quản lý hồ sơ y tế . . . . . . . 56 4.1 Cấu trúc của một quy tắc truy cập đặc tả chính sách hệ thống. . . . 74 4.2 Truy vấn SQL lấy thông tin vai trò - người dùng trong cơ sở dữ liệu của hệ thống quản lý hồ sơ y tế . . . . . . . . . . . . . . . . . . . 79 5.1 Cấu trúc tệp đặc tả chính sách ABAC của hệ thống . . . . . . . . . . 90 5.2 Đoạn mã biểu diễn chính sách ABAC đã đặc tả. . . . . . . . . . . . . 99 5.3 Chính sách ABAC được triển khai. . . . . . . . . . . . . . . . . . . . . 100 5.4 Lễ tân có thể đọc hồ sơ bệnh nhân. . . . . . . . . . . . . . . . . . . . . 101 5.5 Y tá có thể cập nhật hồ sơ bệnh nhân. . . . . . . . . . . . . . . . . . . 103 xiii
Chương 1 GIỚI THIỆU 1.1. Đặt vấn đề Các hệ thống phần mềm hiện đang được tích hợp sâu rộng trong nhiều lĩnh vực của đời sống xã hội. Một số lĩnh vực quan trọng như quân sự, kinh tế, y tế, giáo dục, v.v cũng đều sử dụng phần mềm trong các công việc của họ. Vì vậy, chất lượng của phần mềm có ảnh hưởng trực tiếp hoặc gián tiếp đến người dùng hệ thống. Lợi ích của việc sử dụng phần mềm trong thực tế là không thể phủ nhận, nó giúp con người tiết kiệm thời gian, tiền bạc và công sức. Tuy nhiên, phần mềm hiện nay không chỉ dừng lại ở việc sử dụng trên một máy tính cá nhân mà còn chạy trên các hệ thống có kết nối mạng. Do đó, các hệ thống phần mềm, đặc biệt là các hệ thống web luôn tiềm ẩn các nguy cơ bị tấn công an ninh và khai thác tài nguyên trái phép [99, 102]. Một số lượng lớn các biện pháp, kỹ thuật đã được nghiên cứu ở các giai đoạn để chống lại các cuộc tấn công và bảo vệ các ứng dụng web [54]. Dựa trên nguyên tắc thiết kế và các tính chất an ninh, các kỹ thuật hiện có được chia thành ba nhóm chính: (i) Xây dựng các ứng dụng web an toàn để đảm bảo rằng không có lỗ hổng tiềm ẩn nào tồn tại trong các ứng dụng [11, 25, 51, 81, 82, 105]. Do đó, tài nguyên của hệ thống được bảo vệ và không bị khai thác trái phép. Những nghiên cứu này thường xây dựng các ngôn ngữ lập trình hoặc khung làm việc mới với cơ chế bảo mật, tự động thực thi các tính chất an ninh mong muốn. Các kỹ thuật này giải quyết các vấn đề bảo mật từ gốc và do đó mạnh mẽ nhất. Tuy nhiên, chúng phù hợp nhất để phát triển ứng dụng web mới. (ii) Kiểm chứng các tính chất an ninh mong muốn của ứng dụng web có được đảm bảo hay không và xác định các lỗ hổng tiềm ẩn trong ứng dụng [2, 5, 22, 28, 32, 38, 47, 48, 49, 53, 62, 70, 76, 79, 84, 88, 98, 104]. Với hướng nghiên cứu này, các kỹ thuật phân tích và kiểm tra chương trình thường được áp dụng. Cụ thể, phân tích chương trình bao gồm phân tích tĩnh 1
(kiểm tra/xem xét được thực hiện trên mã nguồn mà không thực thi) và phân tích động (quan sát hành vi thời gian chạy thông qua thực thi). Tuy nhiên, phân tích tĩnh có khả năng trong việc xác định tất cả các lỗ hổng tiềm ẩn nhưng có thể đưa ra các cảnh báo sai. Mặt khác, phân tích động đảm bảo tính đúng đắn của các lỗ hổng được xác định trong không gian được khám phá, nhưng không thể đảm bảo tính đầy đủ. Các kỹ thuật trong hướng này có thể được áp dụng cho cả ứng dụng web mới và cũ. (iii) Bảo vệ một ứng dụng web có khả năng dễ bị tấn công khỏi bị khai thác bằng cách xây dựng một môi trường thực thi an toàn [16, 55, 71, 85]. Các nghiên cứu này thường hướng đến việc sắp đặt các biện pháp bảo vệ (proxy, v.v.) để tách ứng dụng web khỏi các thành phần khác trong hệ sinh thái web, hoặc thiết đặt các thành phần cơ sở hạ tầng (thời gian chạy, trình duyệt web, v.v.) để giám sát hành vi của nó và xác định/cô lập các khai thác tiềm năng. Những kỹ thuật này có thể độc lập với ngôn ngữ lập trình hoặc nền tảng, do đó có thể mở rộng quy mô tốt. Tuy nhiên, chi phí hiệu suất thời gian chạy cần được xem xét. Bên cạnh đó, theo ISO/IEC 27002:20131 , để bảo vệ tài nguyên của các hệ thống phần mềm trước các nguy cơ tấn công an ninh, các nhà phát triển thường phải xây dựng các hệ thống chính sách an ninh cho các phần mềm của họ. Một số biện pháp được thực thi phổ biến gồm: mật mã để đảm bảo sự an toàn và bảo mật thông tin; điều khiển truy cập để hạn chế các vi phạm truy cập đến các tài nguyên của hệ thống; truyền thông an toàn để bảo vệ thông tin trước các nguy cơ đánh chặn hoặc thay thế làm rò rỉ hoặc sai lệch thông tin trong quá trình gửi nhận. Trong thực tế, điều khiển truy cập là một biện pháp cần được thực hiện để đảm bảo tính bảo mật, tính toàn vẹn và tính sẵn sàng của các hệ thống phần mềm [101]. Tuy nhiên, việc triển khai chính sách điều khiển truy cập ở mỗi giai đoạn phát triển phần mềm luôn có khả năng tiềm ẩn các lỗ hổng an ninh. Một trong các nguyên nhân dẫn đến các lỗ hổng an ninh là việc không tuân thủ hoặc bỏ sót các yêu cầu an ninh. Sự không tuân thủ đơn giản nhất có thể là một lỗi hoặc thiếu sót trong lập trình. Điều này rất dễ xảy ra, bởi vì tại giai đoạn lập trình, một hệ thống phần mềm thường có sự kết hợp phức tạp từ nhiều thành phần và thư viện, do đó có thể phát sinh các lỗi tiềm ẩn ngoài mong đợi. Thêm vào đó, người lập trình có thể không phải là người thiết kế và tính biểu đạt cao của ngôn ngữ đặc tả trong bản thiết kế cũng có thể dẫn đến 1 https://www.iso.org/standard/54533.html 2
việc người lập trình hiểu không đầy đủ các yêu cầu đã đặc tả. Tất cả những vấn đề này đều có thể là nguyên nhân dẫn đến việc các hệ thống ứng dụng sẽ không tuân thủ các đặc tả của chúng [56, 9]. Thực tế cho thấy, phần mềm với quy mô càng lớn thì việc triển khai chính sách điều khiển truy cập càng phức tạp và khả năng chứa lỗi càng cao. Bởi vậy, quá trình triển khai chính sách truy cập cần phải được tiến hành, rà soát một cách thận trọng. Do đó, việc kiểm chứng chính sách điều khiển truy cập giữa triển khai và đặc tả của các hệ thống phần mềm là một nhiệm vụ quan trọng, giúp phát hiện sớm các sai sót, đảm bảo các tính chất an ninh của hệ thống và góp phần gia tăng chất lượng của các sản phẩm phần mềm [3, 46]. Các nghiên cứu nhằm giải quyết bài toán này được thực hiện rất đa dạng, phức tạp theo nhiều hướng tiếp cận khác nhau, từ việc xây dựng các mô hình, đặc tả các tính chất an ninh [15, 29, 40] cho đến việc phân tích, thẩm định chính sách điều khiển truy cập ở nhiều giai đoạn trong tiến trình phát triển phần mềm [6, 19, 24, 26, 27, 28, 37, 62, 78, 88]. Ngoài ra, một số phương pháp cũng xây dựng các công cụ phân tích để phát hiện tự động các lỗ hổng bảo mật từ mã nguồn, giúp nhà phát triển hệ thống thực hiện các sửa đổi cần thiết trước khi phần mềm được phát hành [23, 30, 31, 48, 106]. Với bài toán kiểm chứng chính sách điều khiển truy cập theo vai trò, các nghiên cứu [6, 24, 48, 62, 78, 88] chủ yếu tiến hành kiểm tra phép gán giữa các quyền và các vai trò trong hệ thống ở giai đoạn thiết kế hoặc bằng cả kỹ thuật phân tích tĩnh và động từ mã nguồn. Trong khi đó, với điều khiển truy cập theo thuộc tính, một số nghiên cứu [11, 28, 37, 51] đã tập trung đặc tả, triển khai, kiểm thử chính sách điều khiển truy cập của các hệ thống ứng dụng trong thực tế với khung làm việc Spring Security. Tuy nhiên, các nghiên cứu này chưa xác minh tính bảo mật, tính toàn vẹn và tính sẵn sàng của chính sách truy cập được triển khai trong ứng dụng web chỉ bằng phân tích mã nguồn [75, 107]. Vì vậy, 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” đề ra hai mục tiêu chung để nghiên cứu: (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 đặc tả ; (ii) Phát triển các công cụ để hỗ trợ quá trình kiểm chứng tự động. Trong khuôn khổ nghiên cứu, luận án tập trung giải quyết bài toán kiểm tra sự phù hợp giữa triển khai và đặc tả theo hai kịch bản là (i) ứng dụng web có chứa các quy tắc truy cập không có 3
trong đặc tả và (ii) một số quy tắc truy cập đã đặc tả nhưng không được triển khai trong ứng dụng web. Trường hợp vi phạm thứ nhất được hiểu tương đương là người dùng có thừa các chức năng trong hệ thống ứng dụng. Điều này dẫn đến việc người dùng có thể thực hiện nhiều thao tác với tài nguyên hơn so với quy định của tổ chức. Trường hợp vi phạm thứ hai xảy ra khi người dùng không có đủ chức năng trong hệ thống ứng dụng để thực hiện các công việc được giao. Trong hai trường hợp vi phạm truy cập kể trên, trường hợp đầu có ảnh hưởng nghiêm trọng đến tài nguyên của hệ thống. Bởi vì, khi đó tính bảo mật, tính toàn vẹn của hệ thống sẽ không được đảm bảo. Ở trường hợp vi phạm thứ hai, tuy không dẫn đến nguy cơ rò rỉ hoặc làm sai lệch tài nguyên của hệ thống, nhưng khi đó người dùng không hoàn thành được các công việc được giao theo quy định. Do đó, kiểu vi phạm này sẽ làm mất tính sẵn sàng của hệ thống. Để giải quyết bài toán này, luận án giả sử rằng chính sách điều khiển truy cập của hệ thống đã được đặc tả nhất quán và đầy đủ với các yêu cầu của các tổ chức. Các phương pháp chính được sử dụng trong quá trình thực hiện luận án là phân tích mã nguồn, mô hình hóa và so sánh. Ngoài mục đích kiểm tra sự phù hợp của chính sách truy cập được triển khai và đặc tả, các phương pháp đề xuất của luận án còn cung cấp các thông tin về các quy tắc truy cập đã triển khai không chính xác (nếu có) để giúp các nhà lập trình có thể lần vết và thực hiện các điều chỉnh kịp thời. Đối tượng nghiên cứu của luận án là chính sách điều khiển truy cập của hệ thống web. Cụ thể là chính sách điều khiển truy cập theo vai trò và chính sách điều khiển truy cập theo thuộc tính. Đồng thời, luận án quan tâm đến các mô hình biểu diễn, đặc tả chính sách và các phương pháp triển khai chính sách trong hệ thống ứng dụng. Từ đó, mã nguồn của ứng dụng được phân tích, tổng hợp và kiểm chứng. 1.2. Nội dung nghiên cứu Kiểm soát truy cập đã được chứng minh trong thực tiễn là một trong những kỹ thuật hiệu quả để ngăn chặn các vi phạm truy cập nhằm đảm bảo các tính bảo mật, tính toàn vẹn và tính sẵn sàng của các hệ thống phần mềm. Trong thực tế, có nhiều mô hình kiểm soát truy cập đã được đề xuất [50, 83, 101] nhưng điều khiển truy cập theo vai trò (RBAC) và điều khiển truy cập theo thuộc tính (ABAC) là hai mô hình được triển khai phổ biến và hiệu quả trong các hệ thống ứng dụng [44]. Tuy nhiên, việc đảm bảo tính chính xác của những chính sách 4
điều khiển truy cập này được triển khai trong các hệ thống ứng dụng ở giai đoạn lập trình luôn là một thách thức lớn đối với các nhà phát triển phần mềm. Bên cạnh đó, với nhiều thư viện được tích hợp để hỗ trợ cho việc triển khai các chính sách điều khiển truy cập được an toàn, ngôn ngữ lập trình Java cũng được các nhà lập trình thường lựa chọn để phát triển các sản phẩm của họ. Khi đó, chính sách điều khiển truy cập của hệ thống có thể được triển khai theo phương pháp an ninh lập trình và/hoặc an ninh khai báo theo kiến trúc MVC, khung làm việc Spring Security. Vì thế, phạm vi nghiên cứu của luận án là các hệ thống web được phát triển bởi JavaEE theo kiến trúc MVC, khung làm việc Spring Security. Để hoàn thành các mục tiêu đã đề ra, luận án tập trung nghiên cứu các nội dung chính sau: Nghiên cứu các mô hình biểu diễn các chính sách điều khiển truy cập của hệ thống phần mềm: đ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 (SecureUML), điều khiển truy cập theo thuộc tính. Nghiên cứu các phương pháp an ninh lập trình, an ninh khai báo để triển khai chính sách RBAC, ABAC của các hệ thống web theo mô hình kiến trúc MVC, khung làm việc Spring Security. Đề xuất các phương pháp phân tích mã nguồn, biểu diễn chính sách điều khiển truy cập của hệ thống web. Đề xuất các thuật toán kiểm tra sự phù hợp của mô hình chính sách điều khiển truy cập của hệ thống web và đặc tả. Cài đặt các công cụ theo các phương pháp đã đề xuất để hỗ trợ quá trình kiểm chứng tự động. 1.3. Đóng góp của luận án Sau quá trình giải quyết bài toán với mục tiêu, đối tượng và phương pháp nghiên cứu đã đề ra, luận án có các đóng góp chính sau đây: (i) Đề xuất 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. Các phương thức khai thác tài nguyên trong ứng dụng web được trích rút thành danh sách quyền truy cập tài nguyên. Sau đó kết hợp với thành phần Controller và V iew để xây dựng đồ thị khai 5