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

inh 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ắt Từ gốc Giải nghĩa - Tạm dịch ABAC Attribute-Based Access Control Điều khiển truy cập dựa trên thuộc tính API Application Programming Interface Giao diện lập trình ứng dụng 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- trol Điều khiển truy cập tùy ý FSA Finite State Automata Ôtômat hữu hạn trạng thái HTML Hypertext Markup Lan- guage Ngôn ngữ đánh dấu siêu văn bản IEC International Electrotechni- cal Commission Uỷ ban kỹ thuật điện quốc tế ISO International Organization for Standardization Tổ chức tiêu chuẩn hoá quốc tế 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- dards and Technology Viện Tiêu chuẩn và Kĩ thuật Quốc 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- vancement of Structured In- formation Standards Tổ chức cải tiến các tiêu chuẩn thông tin có cấu trúc 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 Markup Language Ngôn ngữ đánh dấu kiểm soát truy cập mở rộng XML Extensible Markup Lan- guage Ngôn ngữ đánh dấu mở rộng 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 1https://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...c cấp quyền của hệ thống này được mô tả trực quan như trong Hình 2.5. Dễ thấy rằng, với SecureUML chính sách điều khiển truy cập theo vai trò đã được mở rộng hơn khi được bổ sung các ràng buộc cấp quyền. Tuy nhiên, với các hệ thống phần mềm, khi mà tiêu chí cấp quyền cho người dùng không chỉ phụ thuộc vào vai trò của họ mà còn phụ thuộc vào các thông tin khác như trình độ chuyên môn hay địa chỉ vật lý mạng của người dùng, thì việc biểu diễn chính sách truy cập của hệ thống với SecureUML rất cồng kềnh và phức tạp. Hoặc với những hệ thống lớn, có sự liên kết giữa nhiều tổ chức, thì mô hình RBAC không thể diễn tả được chính sách điều khiển truy cập của hệ thống. Bởi vì, những 18 > Receptionists > PatientMR actiontype: read > PatientRecord - mrID: String - pID: String - dID: String - contents: String ... + getMrID() + getPID() + getDID() + getContents() + setContents() ... > Patient > ReceptionistMR actiontype: create > User11 > Doctor > User1N > Owner Caller.ID = CalledResource.pID > DoctorMR actiontype1: read actiontype2: update > User2M > User31 > User21 > User3K > Treatment Caller.ID = CalledResource.dID Hình 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. người dùng của tổ chức liên kết sẽ không truy cập được tới tài nguyên hệ thống vì họ không có vai trò trong tổ chức đó. Trong những trường hợp này, mô hình điều khiển truy cập theo thuộc tính sẽ biểu diễn chính sách điều khiển truy cập của hệ thống hiệu quả và linh hoạt hơn. 2.2.3. Điều khiển truy cập theo thuộc tính Điều khiển truy cập theo thuộc tính (ABAC) [41, 42, 45] là mô hình điều khiển truy cập rất linh hoạt và hiệu quả. Trong đó, quyết định truy cập đối với tài nguyên của hệ thống được thực hiện dựa trên các thuộc tính của người dùng, thuộc tính của đối tượng và thuộc tính của môi trường được yêu cầu. NIST (National Institute of Standards and Technology) định nghĩa ABAC là một phương thức điều khiển truy cập, trong đó chủ thể yêu cầu thực hiện các thao tác trên các đối tượng được cấp quyền hoặc từ chối dựa trên các thuộc tính được gán của chủ thể, các thuộc tính được gán của đối tượng, các điều kiện môi trường và một bộ chính sách được xác định đối với các thuộc tính và điều kiện đó. ˆ Các thuộc tính là các thông tin về các đặc điểm của chủ thể, đối tượng hoặc điều kiện môi trường. Chúng được cung cấp bởi một cặp tên - giá trị. 19 ˆ Chủ thể là người dùng hoặc thực thể không phải là người (ví dụ như một thiết bị) đưa ra các yêu cầu truy cập để thực hiện các thao tác trên các đối tượng. Các chủ thể được gán một hoặc nhiều thuộc tính. Đối với nghiên cứu này này, chủ thể và người dùng được hiểu đồng nghĩa. ˆ Đối tượng được hiểu là các tài nguyên của hệ thống. Ví dụ như thiết bị, tệp, bản ghi, bảng, quy trình, chương trình, mạng hoặc miền chứa/nhận thông tin. Nó có thể là thực thể được yêu cầu, cũng như mọi thứ mà một hoạt động có thể được thực hiện bởi một chủ thể bao gồm dữ liệu, ứng dụng, dịch vụ, thiết bị và mạng. ˆ Một phép toán là việc thực hiện một hoạt động nào đó theo yêu cầu của một chủ thể trên một đối tượng. Các hoạt động thường bao gồm đọc, viết, chỉnh sửa, xóa, sao chép, thực hiện và sửa đổi. ˆ Chính sách là sự thể hiện của các quy tắc hoặc các mối quan hệ giúp xác định một yêu cầu truy cập có nên được phép hay không, với các giá trị của các thuộc tính của chủ thể, đối tượng và có thể cả các điều kiện môi trường. ˆ Điều kiện môi trường là bối cảnh hoạt động hoặc tình huống, trong đó yêu cầu truy cập xảy ra. Điều kiện môi trường là đặc điểm môi trường độc lập với chủ thể, đối tượng và có thể bao gồm thời gian hiện tại, ngày trong tuần, vị trí của người dùng hoặc mức độ đe dọa hiện tại. Cơ chế ABAC được mô tả trong Hình 2.6. Trong đó: điểm thực thi chính sách (Policy Enforcement Point - PEP) là nơi thực thi quyết định ủy quyền để đáp Subject Policy Enforcement Point (PEP) Policy Decision Point (PDP) Subject Attribute Object Attribute Object Hình 2.6: Cơ chế điều khiển truy cập theo thuộc tính. 20 ứng các yêu cầu từ các chủ thể; điểm quyết định chính sách (Policy Decision Point - PDP) chịu trách nhiệm đánh giá các yêu cầu của các chủ thể theo các thuộc tính của chủ thể, các thuộc tính của đối tượng và điều kiện môi trường cùng chính sách hiện hành để đưa ra quyết định cấp phép hoặc từ chối yêu cầu của chủ thể. Các thành phần và chính sách cấp quyền trong mô hình ABAC được mô tả hình thức như Định nghĩa 2.2. Định nghĩa 2.2 Mô hình ABAC là một bộ có tám thành phần MABAC = 〈S,RS,E,As,Ars,Ae,OP,P〉. Trong đó: 1. S, RS và E là tập các chủ thể, tài nguyên và môi trường. 2. OP là tập các phép toán có thể được thực hiện trên tài nguyên bởi các chủ thể như: create, read,modify, delete. 3. As, Ars, Ae là tập các thuộc tính của chủ thể s, tài nguyên rs và môi trường e. 4. Một quy tắc truy cập R là một hàm Boolean trên tập các thuộc tính của chủ thể s ∈ S, phép toán op ∈ OP, và tài nguyên rs ∈ RS trong môi trường e ∈ E. R(s, op, rs, e)← f(As, op.name,Ars,Ae) . 5. Chính sách P là tập các quy tắc truy cập được lưu trữ trong kho lưu trữ trung tâm (ví dụ: tệp tin). P = {R1, R2, ..., Rn} Ví dụ: Trong một hệ thống quản lý hồ sơ y tế (hệ thống này sẽ được sử dụng trong phần thực nghiệm của Chương 5), chính sách điều khiển truy cập của hệ thống được phát biểu như sau: Bệnh nhân chỉ được đọc hồ sơ bệnh án của họ; Các bác sĩ chỉ chịu trách nhiệm điều trị cho các bệnh nhân đã được phân công tại chuyên khoa của họ trong bệnh viện. Do đó, các bác sĩ chỉ có quyền đọc và sửa đổi hồ sơ y tế của bệnh nhân mà họ điều trị. Bên cạnh đó, họ cũng có quyền đọc các hồ sơ y tế của bệnh nhân mà họ đang điều trị trong những bệnh viện liên kết; Y tá chỉ có thể đọc hồ sơ các bệnh nhân trong khoa, bệnh viện họ làm việc; Lễ tân có quyền tạo hồ sơ y tế cho những bệnh nhân trong bệnh viện của họ. Mỗi bệnh viện thường có nhiều chuyên khoa để điều trị cho nhiều đối tượng bệnh nhân khác nhau như khoa tim mạch, khoa thần kinh, khoa tai mũi họng, v.v. Các bác sĩ thường làm việc cho một bệnh viện và chịu trách nhiệm điều trị cho một số bệnh nhân trong khoa họ làm việc. Bên cạnh đó, giữa một số bệnh 21 viện thường có sự kết hợp trong khám và điều trị y khoa bằng các thỏa thuận trong việc chia sẻ hồ sơ y tế. Giả sử rằng, mỗi bệnh nhân trong hệ thống chăm sóc sức khỏe này chỉ có một mã định danh và có thể khám nhiều lần tại cùng hoặc khác bệnh viện trong hệ thống liên kết ở các thời điểm khác nhau. Tuy nhiên tại một thời điểm, một bệnh nhân chỉ có một hồ sơ bệnh án và được điều trị tại một bệnh viện. Các thông tin liên quan đến bệnh nhân được mô tả trong hồ sơ bệnh nhân (tài nguyên của hệ thống). Mỗi bác sĩ chỉ làm việc cho một khoa trong một bệnh viện và một bác sĩ có thể điều trị cho nhiều bệnh nhân. Tất cả người dùng tham gia vào hệ thống ứng dụng trong các cơ sở y tế phải tuân thủ chính sách truy cập này. Bên cạnh đó, hệ thống ứng dụng minh họa cho bài toán này có sự kết hợp của hai bệnh viện A và B. Họ có một thỏa thuận hợp tác trong việc chia sẻ thông tin y tế là “Các bác sĩ có thể đọc các hồ sơ y tế của bệnh nhân mà họ đang điều trị ở các bệnh viện liên kết (nếu có)”. Áp dụng Định nghĩa 2.2, mô hình chính sách ABAC của hệ thống quản lý hồ sơ y tếM = 〈S,RS,E,As,Ars,Ae,OP,P〉 được trình bày như sau: ˆ S = {Patients, Doctors, Nurses, Receptionists} ˆ RS = {PatientRecords}; ˆ E = {∅}; ˆ OP = {Create, Read, Update, Delete}. ˆ As = {id, role, department, hospital}. ˆ Ars = {mrId, pId, dId, department, hospital}. ˆ Ae = {∅}; ˆ P = {R1, R2, R3, R4, R5, R6}, trong đó: R1 = (s.role = ′Patient′) ∧ (op = ′Read′) ∧ (rs = ′PatientRecords′) ∧ (s.Id = rs.pId) R2 = (s.role = ′Doctor′) ∧ (op = ′Read′) ∧ (rs = ′PatientRecords′) ∧ (s.Id = rs.pId) ∧ (s.department = rs.department) ∧ (s.hospital = rs.hospital) R3 = (s.role = ′Doctor′) ∧ (op = ′Update′) ∧ (rs = ′PatientRecords′) ∧ (s.Id = rs.dId)∧ (s.department = rs.department)∧ (s.hospital = rs.hospital) R4 = (s.role = ′Doctor′) ∧ (op = ′Read′) ∧ (rs = ′PatientRecords′) ∧ (rs.hospital s.hospital) ∧ (∃ r ∈ rs : ((rs.pID = r.pID) ∧ (r.hospital = s.hospital) ∧ (r.dId = s.Id))) 22 R5 = (s.role = ′Nurse′) ∧ (op = ′Read′) ∧ (rs = ′PatientRecords′) ∧ (s.department = rs.department) ∧ (s.hospital = rs.hospital), R6 = (s.role = ′Receptionist′)∧ (op = ′Create′)∧ (rs = ′PatientRecords′)∧ (s.hospital = rs.hospital) Điều khiển truy cập theo thuộc tính (ABAC) là một thế hệ kỹ thuật điều khiển truy cập mới, được ra đời trong những năm gần đây. Mô hình này cho phép điều khiển truy cập tài nguyên một cách chi tiết hơn bằng cách sử dụng các thuộc tính khác nhau của các phần tử ủy quyền, tạo thuận lợi cho sự hợp tác chính sách trong một doanh nghiệp lớn hoặc giữa nhiều tổ chức, đồng thời cũng cho phép tách rời các chính sách điều khiển truy cập khỏi lôgic ứng dụng. Do đó, mô hình ABAC đặc biệt hiệu quả và phù hợp với các hệ thống ứng dụng lớn, phức tạp. 2.3. Triển khai chính sách điều khiển truy cập trong JavaEE Phương pháp và kiến trúc được sử dụng để triển khai chính sách điều khiển truy cập đã đặc tả vào các ứng dụng web đóng vai trò quan trọng trong việc rà soát mã nguồn để phát hiện các sai sót. Bởi vì, chúng quyết định vị trí và ngữ nghĩa của các mã an ninh truy cập. Bên cạnh đó, có rất nhiều ngôn ngữ lập trình, kiến trúc thiết kế và thư viện hỗ trợ để lập trình các hệ thống web. Tuy nhiên, với ưu thế đa nền tảng (multi platform), Java được sử dụng phổ biến để tạo các ứng dụng desktop, mobile và web. Java có khối lượng thư viện hỗ trợ lớn giúp việc lập trình trở nên dễ dàng hơn. Trong một số thống kê, ngôn ngữ lập trình Java là một trong những ngôn ngữ phổ biến nhất để phát triển các sản phẩm phần mềm [21]. Do đó, mục này sẽ trình bày về phương pháp an ninh lập trình và an ninh khai báo, kiến trúc MVC và Spring Security được sử dụng trong các đề xuất của luận án. 2.3.1. An ninh truy cập trong JavaEE Các tài nguyên cần được bảo vệ của các hệ thống phần mềm thường được lưu trữ trong các hệ thống cơ sở dữ liệu. Vì thế, có ba yếu tố đe dọa đến sự an toàn của hệ thống cơ sở dữ liệu là sự không an toàn của nơi đặt cơ sở dữ liệu, sử dụng trái phép các chức năng của ứng dụng để thực hiện các thao tác với cơ sở dữ liệu nhằm sao chép, thay đổi các tài nguyên trong cơ sở dữ liệu và điểm yếu của hệ quản trị cơ sở dữ liệu [59]. Để bảo vệ hệ thống cơ sở dữ liệu khỏi các mối đe dọa trên, các nhà phát triển có thể sử dụng các phương pháp như chọn 23 nơi an toàn để đặt hệ thống cơ sở dữ liệu, dùng mã (code) để điều khiển truy cập đến cơ sở dữ liệu, hoặc mã hóa dữ liệu để tránh rò rỉ thông tin. An ninh với mã truy cập (code access security) là một giải pháp quan trọng trong các hệ thống cơ sở dữ liệu. Bởi vì, một số vấn đề có thể xảy ra khi người dùng ở máy khách đăng nhập hệ thống bằng cách sử dụng mã được ủy quyền là mã nguồn phía máy khách có thể không đáng tin cậy, có lỗi hoặc bao gồm mã độc. Với giải pháp này, chính sách an ninh của các ứng dụng JavaEE có thể được triển khai theo hai phương pháp là An ninh khai báo, An ninh lập trình hoặc cả hai. ˆ An ninh khai báo (Declarative Security): thể hiện các yêu cầu an ninh của một thành phần ứng dụng bằng các chú thích (annotation) hoặc mã triển khai (deployment descriptor). Mã triển khai có thể được biểu diễn trong tệp *.xml ở bên ngoài ứng dụng để đại diện cho cấu trúc an ninh của ứng dụng. Cấu trúc này bao gồm các thông tin an ninh như vai trò, điều khiển truy cập và các yêu cầu xác thực. Các chú thích được sử dụng để xác định thông tin an ninh trong một tệp tin chứa lớp (file class). Chúng có thể được sử dụng hoặc ghi đè (overwritten) bởi các mã triển khai. Để triển khai theo cách này, người lập trình thường sử dụng các khung làm việc được tích hợp thêm trong các ngôn ngữ lập trình. Các khung làm việc này đã được xác minh về tính chính xác, đúng đắn và dễ sử dụng. Tuy nhiên nó không giải quyết được tất cả mọi nhu cầu về an ninh thực tế. Với nền tảng Java, Spring Security là một trong những khung làm việc cung cấp các tính năng xác thực, ủy quyền và các tính năng an ninh khác cho các ứng dụng doanh nghiệp. ˆ An ninh lập trình (Programmatic Security): được nhúng trong một ứng dụng và được sử dụng để đưa ra quyết định an ninh trong trường hợp an ninh khai báo không đủ để mô tả các mô hình chính sách an ninh của hệ thống. Phương pháp này được sử dụng thông qua ngữ nghĩa của ngôn ngữ lập trình. Tuy nhiên, cách triển khai này thường phức tạp hơn việc sử dụng các chú thích như trong an ninh khai báo nhưng nó đáp ứng được mọi yêu cầu về an ninh. 2.3.2. Một số kiến trúc thiết kế phần mềm trong JavaEE Hiện có nhiều ngôn ngữ lập trình khác nhau được sử dụng để triển khai các ứng dụng web cho các tổ chức như Java, PHP, HTML, v.v. Trong thực tế, Java 24 là một ngôn ngữ mang lại nhiều lợi ích cho các nhà phát triển. Một trong những tính năng quan trọng là tính độc lập nền tảng giúp tiết kiệm nhiều thời gian và công sức. Các ứng dụng được viết bởi Java có thể chạy tự động và linh hoạt trên nhiều hệ điều hành hoặc các thiết bị. Ngoài ra, ngôn ngữ Java còn có mức độ bảo mật cao và được sử dụng rộng rãi trong nhiều lĩnh vực khác nhau [12]. Thêm vào đó là có nhiều thư viện bên thứ ba cung cấp các dịch vụ hữu hiệu trong quá trình xây dựng, phát triển và phân tích phần mềm. 2.3.2.1. Kiến trúc Model-View-Controller Model-View-Controller (MVC) được giới thiệu lần đầu tiên trong Smalltalk’80 bởi Krasner và Pope. Kiến trúc MVC [77, 90] là một mẫu thiết kế phần mềm được sử dụng phổ biến khi phát triển các ứng dụng web với nhiều ngôn ngữ khác nhau (Hình 2.7 mô tả kiến trúc MVC với JavaEE). Những ứng dụng được thiết kế theo kiến trúc MVC có khả năng tái sử dụng mã và phát triển song song một cách hiệu quả. Mục đích của mẫu thiết kế phần mềm này là đạt được sự phân tách giữa ba thành phần Model, View và Controller của một ứng dụng bất kỳ. Controller (servlet) Model (java class) View (.JSP) Database Request Response Hình 2.7: Kiến trúc MVC trong JavaEE. ˆ Model mô tả các bản ghi cơ sở dữ liệu, quản lý dữ liệu ứng dụng. Về cơ bản nó chứa dữ liệu ứng dụng, định nghĩa lôgic, đặc tả chức năng. Model có thể là một đối tượng đơn lẻ hoặc là một số thành phần của các đối tượng quản lý dữ liệu và cho phép giao tiếp cơ sở dữ liệu. Trong các ứng dụng, Model là các lớp ∗.java chứa các phương thức kết nối với cơ sở dữ liệu và tương tác với nguồn dữ liệu. ˆ View gồm các mã như là ∗.jsp chịu trách nhiệm hiển thị các kết quả của dữ liệu được chứa trong Model dưới dạng giao diện đồ họa của người dùng. Nó quy định dạng thức dữ liệu được hiển thị và giao tiếp với Controller. Thêm vào đó, nó cũng cung cấp cách thức để tập hợp dữ liệu từ đầu vào. 25 ˆ Controller là sự kết nối giữa người dùng và hệ thống. Nó điều khiển cả Model và View bằng việc kiểm soát cách dữ liệu phát sinh trong Model và cập nhật View ngay sau khi dữ liệu được thay đổi. Nói cách khác, Controller có chức năng tạo sự đồng bộ giữa Model và View, nó tương tác với Model và lấy dữ liệu để tạo View. Trong một ứng dụng được phát triển bởi J2EE, kiến trúc MVC có thể được sử dụng để tách các chức năng lớp nghiệp vụ được diễn tả bởi Model khỏi chức năng lớp trình diễn được mô tả bởi View bằng việc sử dụng một bộ điều khiển dựa trên một servlet trung gian. Tuy nhiên, một thiết kế Controller phải chứa đầu vào từ các kiểu máy khách khác nhau bao gồm các yêu cầu HTTP từ trang web của máy khách và các tài liệu dựa trên XML từ nhà cung cấp và các bên tham gia. Với mô hình Yêu cầu/Phản hồi HTTP, các yêu cầu từ HTTP đến, được định tuyến tới một bộ điều khiển trung tâm để thông dịch và ủy quyền cho yêu cầu đến các trình xử lý yêu cầu thích hợp. Các trình xử lý yêu cầu được móc vào khung làm việc đã cung cấp cho các nhà phát triển để thực hiện các yêu cầu lôgic cụ thể tương tác với mô hình. Phụ thuộc vào kết quả của tương tác này, bộ điều khiển có thể quyết định View tiếp theo để tạo phản hồi một cách chính xác. 2.3.2.2. Kiến trúc Spring Security Spring Security5 là một khung làm việc hỗ trợ một số cơ chế điều khiển truy cập để bảo đảm các chính sách truy cập cho các ứng dụng phần mềm doanh nghiệp dựa trên nền tảng JavaEE [7, 68, 86]. Kiến trúc tổng quát của Spring Security6 được mô tả trong Hình 2.8, bao gồm các hệ thống con có nhiệm vụ xác thực và ủy quyền. Xác thực có trách nhiệm kiểm tra tính hợp pháp của người dùng và ủy quyền sẽ quyết định quyền truy cập tài nguyên cho người dùng hợp pháp thông qua vai trò của họ. Spring Security cho phép người lập trình cấu hình cả với Java và XML. Do đó, chính sách truy cập của hệ thống có thể được thực thi theo các quy tắc điều khiển truy cập dựa trên URL trong môi trường web hoặc ở cấp độ của phương thức Java. Điều này có nghĩa là các nhà phát triển có thể chọn lựa giữa các cấu hình an ninh dựa trên XML, Java hoặc kết hợp cả hai. Cấu hình dựa trên XML thực thi các yêu cầu an ninh với các mã triển khai và mã nguồn, trong khi các 5https://spring.io/projects/spring-security 6https://cms.einnovator.org/publication/spring-security 26 Hình 2.8: Kiến trúc tổng quát của Spring Security. phương thức dựa trên Java được thực hiện với các chú thích và mã. Bởi vì, Spring Security chỉ hỗ trợ trực tiếp việc triển khai chính sách RBAC cho nên chính sách ABAC sẽ được triển khai theo cả phương pháp an ninh lập trình và an ninh khai báo. Hình 2.9 mô tả khung làm việc của Spring khi triển khai mô hình điều khiển truy cập theo thuộc tính trong các ứng dụng được lập trình từ JavaEE [11]. Trong đó, chính sách ABAC của ứng dụng web được biểu diễn dưới dạng tập quy tắc truy cập viết bằng ngôn ngữ biểu thức Spring và lưu trữ trong tệp tin *.json. Với kiến trúc này, người lập trình ứng dụng phải cài đặt thêm các hàm hasPermission như Đặc tả 2.1 và CheckPermission như Đặc tả 2.2 để tạo ra một bộ lọc cho Spring nhằm đánh giá quyền của các vai trò khi thực thi chính sách. Security Context Resources @PreAuthorize(“can_do()”) Method call Security Interceptor Security Context Handler Authentication Manager Authorization Manager User Customized Spring Security SpEL evaluator ABAC Policy SecurityMetadata (ConfigAttribute) Authorization Object Hình 2.9: Kiến trúc Spring triển khai ABAC trong JavaEE. 27 Đặc tả 2.1: Mã nguồn của hàm hasPermission public boolean hasPermission(Authentication authentication , Object targetDomainObject, Object permission) { User user = userRepository.findByUsername(authentication.getName()); Map environment = new HashMap(); ronment.put("time", new Date()); logger.debug("hasPersmission({}, {}, {})", user, targetDomainObject, permission); return policy.check(user, targetDomainObject, permission, environment); } @Override public boolean hasPermission(Authentication authentication, Serializable targetId, String targetType, Object permission) { return false; } Đặc tả 2.2: Mã nguồn của hàm checkPermission public class ContextAwarePolicyEnforcement { @Autowired protected PolicyEnforcement policy; @Autowired private UserRepository userRepository; public void checkPermission(Object resource, String permission) { Authentication auth = SecurityContextHolder.getContext().getAuthentication(); User user = userRepository.findByUsername(auth.getName()); Map environment = new HashMap(); environment.put("time", new Date()); if(!policy.check(user, resource, permission, environment)) throw new AccessDeniedException("Access is denied"); } } Trong đoạn mã nguồn trên, hai hàm hasPermission có đầu vào khác nhau và đều thuộc lớp AbacPermissionEvaluator được triển khai (implements) từ lớp PermissionEvaluator. Vì chỉ cần sử dụng hàm hasPermission(Authentication authentication , Object targetDomainObject, Object permission) trong quá trình 28 triển khai chính sách ABAC nên hàm này được cài đặt lại còn hàm hasPer- mission(Authentication authentication, Serializable targetId, String targetType, Object permission) luôn được trả về giá trị false. Cả hai hàm hasPermission và checkPermission đều có lời gọi đến policy.check() để đối chiếu thông tin từ yêu cầu tài nguyên của các chủ thể với các quy tắc truy cập ABAC được lưu trữ trong tệp .json. 2.4. Phân tích và biểu diễn chương trình Kiểm soát truy cập là biện pháp hiệu quả để hạn chế các vi phạm truy cập. Tuy nhiên, nó không phải là một giải pháp hoàn chỉnh để bảo vệ tài nguyên hệ thống. Bởi vì, nếu chính sách truy cập của hệ thống không được triển khai chính xác trong từng giai đoạn phát triển phần mềm thì vẫn phát sinh các lỗ hổng an ninh trong các sản phẩm phần mềm và xảy ra các vi phạm truy cập tài nguyên. Thực tế là, khoảng một nửa các khiếm khuyết dẫn đến các lỗ hổng an ninh được tìm thấy trong phần mềm hiện nay thực sự là do các lỗ hổng trong kiến trúc, thiết kế và lập trình [52, 64]. Các sai sót có thể xuất hiện trong suốt vòng đời phát triển của phần mềm. Nếu sai sót không được phát hiện, nó có thể trở thành các lỗ hổng an ninh ở thời điểm thực thi và có thể bị những kẻ tấn công khai thác các tài nguyên quan trọng hoặc phá hoại hệ thống dẫn đến hàng loạt tổn thất nghiêm trọng. Do đó, điều khiển truy cập cần phải được kết hợp với các công việc kiểm tra, rà soát. Trong nghiên cứu [64], với mục tiêu làm giảm số lượng các sai sót càng sớm càng tốt đồng thời giảm thiểu sự nhập nhằng và những điểm yếu khác, tác giả McGraw đã giới thiệu một số hoạt động áp dụng tốt nhất để đảm bảo chính sách an ninh phần mềm tại các giai đoạn của vòng đời phát triển phần mềm (Software Development Life Cycle) theo thứ tự hiệu quả của chúng, được chỉ ra trong Hình 2.10. Code Review Risk Analysis 2 Design Test Plans Requirements and use cases Code Test results Field feedback 1 Risk Analysis 2 Penetration Testing 3 Risk - Based Security Tests 4 Abuse Cases 5 Security Requirements 6 Security Operations 7 Hình 2.10: Các hoạt động đảm bảo chính sách an ninh phần mềm. 29 ˆ Rà soát mã nguồn (Code review): Hoạt động được thực hiện ở giai đoạn lập trình bằng kỹ thuật phân tích tĩnh. Phương pháp tập trung vào các lỗi triển khai đặc biệt là các lỗ hổng phổ biến. ˆ Phân tích rủi ro kiến trúc (Architectural risk analysis): Hoạt động được thực hiện ở giai đoạn thiết kế và kiến trúc. Hệ thống phải được kết hợp và thể hiện ở một hình thái thống nhất. Nhà thiết kế, kiến trúc sư và nhà phân tích cần ghi chép rõ ràng các giả định và xác định các cuộc tấn công có thể xảy ra để tránh các lỗi thiết kế. ˆ Kiểm thử thâm nhập (Penetration testing): Hoạt động này là cực kỳ hữu ích, đặc biệt nếu là một phân tích rủi ro kiến trúc. Phương pháp mang lại sự hiểu biết tốt về phần mềm trong môi trường thực. ˆ Kiểm thử an ninh dựa trên rủi ro (Risk-based security tests): Một kế hoạch kiểm tra an ninh tốt phải bao gồm cả hai chiến lược (i) kiểm thử chức năng an ninh với các kỹ thuật kiểm thử chức năng chuẩn và (ii) kiểm thử rủi ro an ninh dựa trên các mô hình tấn công, kết quả phân tích rủi ro và các trường hợp lạm dụng. ˆ Các trường hợp lạm dụng (Abuse cases): Xây dựng các trường hợp lạm dụng là một cách hữu ích vì các trường hợp lạm dụng mô tả hành vi của hệ thống đang bị tấn công. Tuy nhiên, hoạt động cần có sự tham gia của chuyên gia an ninh nhiều kinh nghiệm vì nó đòi hỏi phải hiểu rõ về những gì cần được bảo vệ, từ ai và trong bao lâu. ˆ Các yêu cầu an ninh (Security requirements): Các yêu cầu an ninh phải được thể hiện rõ ràng, chi tiết. Bao gồm cả an ninh chức năng (ví dụ cách sử dụng mật mã được áp dụng) và các đặc điểm nổi bật (ví dụ các trường hợp lạm dụng và mô hình tấn công). ˆ Các hoạt động an ninh (Security operations): Sử dụng kinh nghiệm của các chuyên gia để phòng ngừa các các tấn công an ninh. 2.4.1. Phân tích chương trình Phân tích chương trình là một trong những phương pháp để hiểu chương trình và phát hiện các lỗi ở giai đoạn lập trình. Một số lỗi lập trình có thể được phát hiện bằng trình biên dịch, khi đó trình biên dịch cung cấp các thông tin liên quan đến lỗi được phát hiện để người lập trình khắc phục và tiến trình phát 30 triển được tiếp tục. Tuy nhiên, việc phát hiện lỗi bằng trình biên dịch không thể áp dụng với hầu hết các lỗ hổng an ninh. Phân tích chương trình là phương pháp phổ biến được sử dụng để kiểm tra việc triển khai chính sách an ninh của các hệ thống phần mềm ở giai đoạn lập trình. Có hai kỹ thuật phân tích chương trình là phân tích tĩnh và phân tích động. ˆ Sức mạnh của các phân tích động nằm ở khả năng nắm bắt hành động hiện có của các đầu vào động. Kiểu phân tích này sẽ xem xét chương trình ở mức tổng quát. Do đó, nó cần đến các phương pháp khác nhau để phân tích hành vi của chương trình tại thời điểm thực thi và thường không có bất cứ truy cập nào tới mã nguồn. Phương pháp này cần đủ lượng ca kiểm thử và tốn khá nhiều thời gian, mà không thể đảm bảo kiểm chứng tự động hay bao quát đầy đủ không gian ca kiểm thử của chương trình được phân tích. Phân tích động báo cáo các lỗi tại trường hợp nó xảy ra, và cung cấp các thông tin chi tiết cho phép người phát triển/người kiểm thử thực hiện các sửa chửa cần thiết. ˆ Phân tích tĩnh đảm bảo bao quát đầy đủ các nhánh của chương trình, sự phụ thuộc chương trình, hoặc các tệp cấu hình được khai thác. Phân tích tĩnh cung cấp các phương pháp luận khác nhau, bao gồm kiểm chứng mô hình, chứng minh mô hình, để xác định các đường thực thi của một chương trình mà không phải thực hiện nó thực sự. Không giống như rà soát thủ công, các bộ phân tích mã tĩnh có thể nắm bắt toàn diện và chính xác các mô hình của phần mềm, ví dụ như một biểu diễn trừu tượng của tất cả các đường thực thi. Nhiều nhà phát triển dựa vào kiểm thử để đảm bảo sự an toàn của các chương trình của họ nhưng không đảm bảo các tính chất an ninh cho phần mềm đã phát triển. Bởi vì, việc kiểm thử chỉ đáp ứng được các yêu cầu chức năng ở giai đoạn cuối của tiến trình phát triển phần mềm khi phần mềm có thể thực thi chứ không phải ở dạng mã nguồn hay byte-code. Không giống như kiểm thử, phân tích mã tĩnh có thể được áp dụng với các tệp đơn lẻ hoặc toàn bộ mã nguồn và không phải đợi khi hoàn thành sản phầm do đó kỹ thuật này có thể sử dụng ở giai đoạn sớm của quá trình phát triển [58]. 2.4.1.1. Một số phương pháp phân tích tĩnh Các bộ phân tích tĩnh được sử dụng cho nhiều mục đích khác nhau như là dò tìm các lỗ hổng an ninh, phát hiện lỗi, kiểm chứng các tính chất an ninh cũng 31 như để hiểu chương trình. Sau đây là một số phương pháp hình thức phổ biến để biểu diễn chương trình và được sử dụng trong phân tích tĩnh. ˆ Phân tích luồng điều khiển (Control Flow Analysis): là một trong các kỹ thuật được sử dụng phổ biến để phân tích mã tĩnh. Luồng điều khiển chương trình được mô hình hóa thành một đồ thị luồng điều khiển (Control Flow Graph - CFG), được giới thiệu đầu tiên bởi Frances E. Allen năm 1970. Đồ thị luồng điều khiển là đồ thị có hướng được sử dụng để biển diễn các khối mã dưới dạng các nút, sự phụ thuộc điều khiển tạo thành các cạnh có hướng, bắt đầu với một nút vào và kết thúc với điểm cuối của chương trình. Việc xây dựng đồ thị luồng điều khiển có thể được thực hiện dựa vào đồ thị cú pháp trừu tượng như là cây cú pháp trừu tượng (Abstract Syntax Tree - AST) [94, 93]. Đặc trưng chính của kỹ thuật này là xác định các thủ tục trong một chương trình gọi lẫn nhau như thế nào cũng như xác định hàm nào được gọi một cách hiệu quả. ˆ Phân tích luồng dữ liệu (Data Flow Analysis): dựa trên biểu diễn trừu tượng của ngữ nghĩa chương trình được phân tích, và tập trung vào trích rút các giá trị có thể của dữ liệu nhằm biểu diễn sự phụ thuộc của dữ liệu trong mã nguồn, và cho phép theo dõi hiệu ứng của dữ liệu vào. Phân tích luồng dữ liệu có mục tiêu dự đoán tĩnh hành vi động của chương trình được phân tích [36]. 2.4.1.2. Một số công cụ phân tích tĩnh Các công cụ phân tích tĩnh được sử dụng chủ yếu trong mục tiêu phát hiện các lỗ hổng an ninh từ mã nguồn, do đó nhà phát triển có thể thực hiện các sửa đổi cần thiết đối với các lỗ hổng an ninh được xác định trước khi phần mềm được phát hành cho khách hàng. Một số công cụ phân tích mã tĩnh là MOPS, SPlint, GraphMatch, Fortify. ˆ MOPS (Model checking Program for Security Properties) [23]: sử dụng kỹ thuật kiểm chứng mô hình để kiểm tra sự vi phạm các quy tắc an ninh được định nghĩa như các tính chất an toàn theo thời gian. Nó dựa trên phương pháp mô hình hóa hình thức cho cả chương trình và các tính chất an ninh, sau đó tiến hành phân tích các mô hình đã triển khai. MOPS mô hình hóa chương trình thành dạng ôtômat đẩy xuống (Push Down Automaton - PDA) chứa tất cả các đường thực thi có thể. PDA được sử dụng như công 32 cụ để phân tích các chương trình. MOPS sử dụng phương pháp này để mô hình các tính chất an ninh thành ôtômat hữu hạn trạng thái (Finite State Automata - FSA) để sắp xếp trật tự chuỗi các thao tác liên quan đến an ninh. Phương pháp này phân chia các tính chất an ninh phức tạp thành các đơn vị nhỏ hơn và có thể sử dụng lại các tính chất an ninh cơ bản, điều này để dễ dàng mô hình hóa và mở rộng. MOPS xác minh rằng các tính chất an ninh được thực hiện chính xác trong tất cả các đường thực thi của chương trình được phân tích, sử dụng kiểm chứng mô hình trên PDA và kiểm tra liệu các trạng thái rủi ro có thể xảy ra trong PDA. ˆ SPlint (Secure Programming LINT) [31] là một bộ phân tích mã tĩnh luồng dữ liệu dựa trên chú thích cho các lỗ hổng an ninh và phát hiện lỗi lập trình của ngôn ngữ C. Nó sử dụng các chú thích (giải nghĩa) đã đưa vào bởi người phát triển. Các chú thích nhằm đặc tả các ràng buộc (tính chất) về một thư viện, một biến, một hàm hoặc một kiểu. Các chú thích biểu diễn tiền điều kiện và hậu điều kiện bên trong thủ tục về các tài nguyên. Sự thực hiện SPlint là một quá trình lặp giúp người phát...ng pháp an ninh khai báo. Sự phù hợp của chính sách điều khiển truy cập và các ràng buộc cấp quyền trong các ứng dụ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. Việc kiểm tra phép gán còn lại, các quy tắc truy cập của ứng dụ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 của ứng dụng. Cuối cùng, hai thuật toán được đề xuất để thực hiện kiểm tra tính chính xác của các phép gán đã được triển khai trong ứng dụng. Một công cụ đã được phát triển để hỗ trợ quá trình kiểm chứng tự động với hệ thống quản lý hồ sơ y tế theo phương pháp đã đề xuất. (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. Quá trình kiểm chứng được thực hiện từ việc trích rút, phân tích các quy tắc truy cập của ứng dụng web. Chính sách điều khiển truy cập theo thuộc tính trong các ứng dụng web được kiểm chứng 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 của chính sách truy cập. Từ phương pháp đề xuất, một công cụ kiểm chứng đã được phát triển để thực hiện quá trình kiểm chứng tự động và thực nghiệm với hệ thống quản lý hồ sơ y tế. Như vậy, luận án đã tập trung giải quyết bài toán kiểm chứng chính sách điều khiển truy cập cho các hệ thống web được phát triển bởi J2EE theo kiến trúc MVC và thư viện Spring Security. Trong đó, chính sách RBAC, ABAC của hệ thống đượ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 đạt được ở trên cho thấy các phương pháp đề xuất đã đáp ứng đầy đủ các mục tiêu nghiên cứu của luận án và góp phần bổ sung và hoàn thiện các phương pháp phân tích, biểu diễn, kiểm tra chính sách truy cập của các ứng dụng web và làm tăng tính tin cậy của hệ thống. Bên cạnh đó, các phương pháp đã được đề xuất trong luận án đều được triển khai thành các công cụ và thực 109 nghiệm với hệ thống quản lý hồ sơ y tế và bước đầu cho các kết quả đúng như dự kiến. Dựa trên các tính chất an ninh, kỹ thuật phân tích được sử dụng và đặc điểm của các hệ thống web mà các phương pháp đề xuất đã thực hiện, khả năng của các phương pháp và công cụ mà luận án đề xuất được tổng hợp, so sánh với các nghiên cứu hiện có trong bảng tổng hợp sau: Bảng 6.1: Bảng so sánh các phương pháp đề xuất và một số nghiên cứu khác. Phương pháp kiểm chứng Tiêu chí Phương pháp đề xuất Một số phương pháp hiện có R B A C C h eck in g V eR A A P V er P isto ia2 0 0 7 R o le [7 6 ] A lalfi2 0 1 2 A u to m ated [5 ] S erg eev 2 0 1 7 A p p ro ach [8 8 ] Jh a2 0 1 8 S p ecificatio n [4 9 ] Mô hình chính sách điều khiển truy cập RBAC SecureUML ABAC RBAC SecureUML SecureUML ABAC Phương pháp thực hiện Phân tích tĩnh Phân tích tĩnh Phân tích tĩnh Phân tích tĩnh Phân tích tĩnh + Động Phân tích tĩnh Kiểm chứng mô hình Phương pháp triển khai chính sách truy cập An ninh lập trình An ninh khai báo An ninh lập trình + An ninh khai báo An ninh lập trình An ninh lập trình An ninh khai báo Kiến trúc, thư viện phát triển hệ thống MVC MVC, Spring Security MVC, Spring Security Spring Security Ngôn ngữ phát triển hệ thống Java EE Java EE Java EE Java EE Java EE Java EE Mô hình biểu diễn chính sách truy cập triển khai Ma trận Cây Tập hợp Đồ thị lời gọi Biểu đồ Biểu đồ Dữ liệu đầu vào Mã nguồn Mã nguồn, Cơ sở dữ liệu Mã nguồn Mã nguồn Mã nguồn, Cơ sở dữ liệu Mã nguồn Trạng thái ABAC, chính sách SoD Kết quả đầu ra Kiểm tra thừa, thiếu quyền được gán cho các vai trò Kiểm tra thừa, thiếu người dùng, vai trò và quyền của các vai trò Kiểm tra tính bảo mật, tính toàn vẹn và tính sẵn sàng Kiểm tra tính thiếu, tính dư thừa, tính phá vỡ Kiểm tra truy cập trái phép, Bảo trì ứng dụng web, Tái cấu trúc ứng dụng web Mô hình SecureUML Kiểm tra các sửa đổi trong thực thi SoD Ngoài ra các phương pháp đề xuất trong luận án cũng tiến hành thực nghiệm với hệ thống quản lý hồ sơ y tế và đo đạc với máy tính xách tay có dung lượng RAM 8 GB, vi xử lý Intel Core i5 - 6300U 2.4GHz. Một số kết quả thống kê được ghi nhận như bảng sau: 110 Bảng 6.2: Bảng kết quả thực nghiệm của các công cụ đề xuất. Phương pháp đề xuất Khả năng phát hiện sai sót Số vai trò, quyền, tài nguyên Kích thước hệ thống web Thời gian kiểm chứng khi không có sai sót (s) RBACChecking - Thừa, thiếu quyền của các vai trò. 3, 3, 1 40,47 MB (40.689.622 bytes) 81 Files, 22 Folders 4 VerRA - Thừa , thiếu người dùng/vai trò. - Thừa, thiếu quyền của các vai trò. 3, 3, 1 71,7 MB (75.282.117 bytes), 162 Files, 57 Folders 4 APVer - Thừa, thiếu quyền theo các thuộc tính. 4, 3, 1 75,0 MB (78.746.748 bytes), 167 Files, 57 Folders 3 Các kết quả của luận án đã được công bố trong ba hội nghị trong và ngoài nước, đã gửi và được chấp nhận bởi một tạp chí chuyên ngành trong nước và một tạp chí quốc tế. 6.2. Hướng phát triển Thực tế cho thấy, việc áp dụng các kỹ thuật, phương pháp để đảm bảo chính sách điều khiển truy cập được triển khai chính xác trong các giai đoạn phát triển của phần mềm là vấn đề rất quan trọng. Bước đầu, luận án mới tập trung giải quyết bài toán mà chính sách của hệ thống được biểu diễn bằng mô hình RBAC, SecureUML, ABAC. Các tính chất an ninh mà luận án thực hiện được mới chỉ bao gồm tính bảo mật, tính toàn vẹn và tính sẵn sàng. Luận án đã đề xuất được một số phương pháp để biểu diễn hình thức, phân tích, kiểm tra các chính sách truy cập từ mã nguồn của một số ứng dụng web. Tuy nhiên, các phương pháp phân tích đã đề xuất còn phụ thuộc vào kiến trúc thiết kế, thư viện sử dụng, phương pháp triển khai chính sách truy cập cũng như ngôn ngữ lập trình khi xây dựng các ứng dụng web,... Vì vậy, đối với mỗi bài toán đã nghiên cứu vẫn còn một số hướng có thể xem xét và phát triển. Một số hướng nghiên cứu tiếp theo của luận án có thể tiến hành là: (i) Quy mô của các hệ thống quản lý hồ sơ y tế được sử dụng trong các thực nghiệm còn đơn giản và chưa phải là các hệ thống thực tế đang được sử dụng trong các tổ chức. Do đó, các hệ thống ứng dụng có khả năng chưa bao quát được hết các tình huống có thể xảy ra vi phạm truy cập tài nguyên trong thực tế. Các số liệu trong quá trình thực nghiệm chưa được tập hợp, so sánh và đánh giá một cách chi tiết. Vì vậy, cần tiếp tục tiến hành các thực nghiệm và đo đạc với các hệ thống khác, lớn hơn có cùng kiến trúc, 111 từ đó có thể xem xét và cải tiến các phương pháp đề xuất để phù hợp với một lớp các bài toán lớn hơn. (ii) Các phương pháp đề xuất trong luận án đều chưa giải quyết các vấn đề liên quan đến truy vết và lưu trữ các hoạt động của người dùng trong các ứng dụng web. Vì thế, các tính chất an ninh mà luận án đã đề cập và giải quyết được mới chỉ dừng lại ở tính bảo mật, tính toàn vẹn và tính sẵn sàng. Do đó, trong các nghiên cứu tiếp theo, luận án có thể tiếp tục mở rộng để triển khai với các tính chất an ninh khác như tính trách nhiệm, tính chống chối bỏ, v.v. (iii) Trong các phương pháp kiểm chứng chính sách RBAC, luận án chưa giải quyết được các vấn đề liên quan đến thừa kế vai trò và cấp phát động các quyền, vai trò cho người dùng được triển khai trong ứng dụng web. Ngoài ra, vấn đề xung đột các quyền theo các phương pháp triển khai chính sách khác nhau cũng chưa được luận án xem xét giải quyết. Vì thế, các phương pháp đề xuất cần được tiếp tục xem xét, mở rộng để giải quyết những vấn đề này trong tương lai. (iv) Tính tối ưu của các thuật toán, dung lượng bộ nhớ cần sử dụng trong các phương pháp đề xuất chưa được xem xét. Tính đúng đắn của các phương pháp đề xuất mới chỉ được thực hiện thông qua các thực nghiệm mà chưa được chứng minh bằng các phương pháp hình thức. Vì vậy, các nghiên cứu tiếp theo có thể xem xét và hoàn thiện các vấn đề này. (v) Hiệu quả của các phương pháp kiểm chứng đã đề xuất phụ thuộc chủ yếu vào các bước phát hiện và xây dựng mô hình chính sách điều khiển truy cập từ mã nguồn ứng dụng. Do đó, việc xây dựng các phương pháp để đánh giá thực nghiệm chi tiết hơn về bước này với các độ đo định lượng là cần thiết trong các nghiên cứu tiếp theo. (vi) Các phương pháp kiểm chứng đề xuất chỉ áp dụng với những hệ thống web mà chính sách RBAC, ABAC của chúng được triển khai theo phương pháp an ninh lập trình, an ninh khai báo với kiến trúc MVC, khung làm việc Spring Security. Điều này làm hạn chế khả năng áp dụng của luận án. Để khả năng áp dụng của các phương pháp đề xuất được tốt hơn, việc xây dựng các bộ ánh xạ để chuyển đổi tương đương giữa các ngôn ngữ lập trình, khung làm việc của các thư viện và kiến trúc thiết kế là cần thiết trong tương lai. 112 Danh mục các công trình khoa học 1. Thanh-Nhan Luong, Van-Khanh To, and Ninh-Thuan Truong, Checking Compliance of Program with SecureUML Model, Advanced Topics in Intelligent Information and Database Systems, Springer, pp. 489-498, (2017). 2. Thanh-Nhan Luong, Dinh-Hieu Vo, Van-Khanh To, and Ninh-Thuan Truong, On the Compliance of Access Control Policies in Web Applications, ICCASA 2018/ICTCC 2018, LNICST 266, pp. 58-69, (2018). 3. Thanh-Nhan Luong, Dinh-Hieu Vo, and Ninh-Thuan Truong, An ap- proach to analyze software security requirements in ABAC model, 2019 6th NAFOSTED Conference on Information and Computer Science (NICS), IEEE, pp. 184-189, (2019). 4. Thanh-Nhan Luong, and Ninh-Thuan Truong, VeRA: Verifying RBAC and authorization constraints models of web applications, International Journal of Software Engineering and Knowledge Engineering (accepted), ISI index. 5.Thanh-Nhan Luong, Thi-Dao Vu, Dinh-Hieu Vo, and Ninh-Thuan Truong, A Tool Support for Checking ABAC Policies in Web Applications, VNU Journal of Science: Computer Science and Communication Engineering (accepted). Danh mục này gồm 05 công trình. 113 Tài liệu tham khảo [1] Abdallah, A.E., Khayat, E.J.: A formal model for parameterized role-based access control. In: IFIP World Computer Congress, TC 1. pp. 233–246. Springer (2004) [2] Ahmadi, H., Small, D.: Graph Model Implementation of Attribute-Based Access Control Policies. arXiv preprint arXiv:1909.09904 (2019) [3] Alalfi, M.H., Cordy, J.R., Dean, T.R.: A survey of analysis models and methods in website verification and testing. In: International Conference on Web Engineering. pp. 306–311. Springer (2007) [4] Alalfi, M.H., Cordy, J.R., Dean, T.R.: A verification framework for access control in dynamic web applications. In: Proceedings of the 2nd Canadian Conference on Computer Science and Software Engineering. pp. 109–113. ACM (2009) [5] Alalfi, M.H., Cordy, J.R., Dean, T.R.: Automated verification of role-based access control security models recovered from dynamic web applications. In: Web Systems Evolution (WSE), 2012 14th IEEE International Symposium on. pp. 1–10. IEEE (2012) [6] Alalfi, M.H., Cordy, J.R., Dean, T.R.: Recovering role-based access control security models from dynamic web applications. In: International Confer- ence on Web Engineering. pp. 121–136. Springer (2012) [7] Alex, B., Taylor, L.: Spring Security Reference Documentation 3.2.0 (2013) [8] Ali, K., Lhoták, O.: Application-only call graph construction. In: Euro- pean Conference on Object-Oriented Programming. pp. 688–712. Springer (2012) [9] Anand, P.: Overview of root causes of software vulnerabilities-technical and user-side perspectives. In: 2016 International Conference on Software Se- curity and Assurance (ICSSA). pp. 70–74. IEEE (2016) [10] Andronick, J., Chetali, B., Paulin-Mohring, C.: Formal verification of se- curity properties of smart card embedded source code. FM 3582, 302–317 (2005) [11] Armando, A., Carbone, R., Chekole, E.G., Ranise, S.: Attribute based ac- cess control for APIs in spring security. In: Proceedings of the 19th ACM symposium on Access control models and technologies. pp. 85–88. ACM (2014) [12] Arnold, K., Gosling, J., Holmes, D.: The Java programming language. Ad- dison Wesley Professional (2005) 114 [13] Basin, D., Clavel, M., Doser, J., Egea, M.: A metamodel-based approach for analyzing security-design models. In: International Conference on Model Driven Engineering Languages and Systems. pp. 420–435. Springer (2007) [14] Basin, D., Doser, J., Lodderstedt, T.: Model driven security: From UML models to access control infrastructures. ACM Transactions on Software Engineering and Methodology (TOSEM) 15(1), 39–91 (2006) [15] Besson, F., Jensen, T., Le Métayer, D., Thorn, T.: Model checking security properties of control flow graphs. Journal of computer security 9(3), 217– 250 (2001) [16] Bisht, P., Sistla, A.P., Venkatakrishnan, V.: Automatically preparing safe SQL queries. In: International Conference on Financial Cryptography and Data Security. pp. 272–288. Springer (2010) [17] Biswas, P., Sandhu, R., Krishnan, R.: Attribute transformation for attribute-based access control. In: Proceedings of the 2nd ACM Workshop on Attribute-Based Access Control. pp. 1–8 (2017) [18] Boadu, E.O., Armah, G.K.: Role-Based Access Control (Rbac) Based In Hospital Management. International Journal of Software Engineering and Knowledge Engineering 3, 53–67 (2014) [19] Castelluccia, D., Mongiello, M., Ruta, M., Totaro, R.: Waver: A model checking-based tool to verify web application design. Electronic notes in theoretical Computer Science 157(1), 61–76 (2006) [20] Charles, P., Pfleeger, S.L.: Analyzing Computer Security: A Threat/vul- nerability/countermeasure Approach. Prentice Hall (2012) [21] Chatley, R., Donaldson, A., Mycroft, A.: The next 7000 programming lan- guages. In: Computing and Software Science, pp. 250–282. Springer (2019) [22] Chaudhuri, A., Foster, J.S.: Symbolic security analysis of ruby-on-rails web applications. In: Proceedings of the 17th ACM conference on Computer and communications security. pp. 585–594 (2010) [23] Chen, H., Wagner, D.: MOPS: an infrastructure for examining security properties of software. In: Proceedings of the 9th ACM conference on Com- puter and communications security. pp. 235–244. ACM (2002) [24] Choi, E.H., Watanabe, H.: Model checking class specifications for web ap- plications. In: Software Engineering Conference, 2005. APSEC’05. 12th Asia-Pacific. pp. 9–pp. IEEE (2005) [25] Chong, S., Vikram, K., Myers, A.C., et al.: SIF: Enforcing Confidentiality and Integrity in Web Applications. In: USENIX Security Symposium. pp. 1–16 (2007) 115 [26] Di Sciascio, E., Donini, F.M., Mongiello, M., Piscitelli, G.: AnWeb: a sys- tem for automatic support to web application verification. In: Proceedings of the 14th international conference on Software engineering and knowledge engineering. pp. 609–616. ACM (2002) [27] Di Sciascio, E., Donini, F.M., Mongiello, M., Totaro, R., Castelluccia, D.: Design verification of web applications using symbolic model checking. In: International Conference on Web Engineering. pp. 69–74. Springer (2005) [28] Dikanski, A., Steinegger, R., Abeck, S.: Identification and Implementa- tion of Authentication and Authorization Patterns in the Spring Security Framework. In: The Sixth International Conference on Emerging Security Information, Systems and Technologies (SECURWARE 2012) (2012) [29] Drouineaud, M., Bortin, M., Torrini, P., Sohr, K.: A first step towards formal verification of security policy properties for RBAC. In: Fourth In- ternational Conference onQuality Software, 2004. QSIC 2004. Proceedings. pp. 60–67. IEEE (2004) [30] D’Souza, D., Kim, Y.P., Kral, T., Ranade, T., Sasalatti, S.: Tool evaluation report: Fortify (2014) [31] Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE software 19(1), 42–51 (2002) [32] Felmetsger, V., Cavedon, L., Kruegel, C., Vigna, G.: Toward automated detection of logic vulnerabilities in web applications. In: USENIX Security Symposium. vol. 58 (2010) [33] Ferraiolo, D., Kuhn, D.R., Chandramouli, R.: Role-based access control. Artech House (2003) [34] Ferraiolo, D.F., Sandhu, R., Gavrila, S., Kuhn, D.R., Chandramouli, R.: Proposed NIST standard for role-based access control. ACM Transactions on Information and System Security (TISSEC) 4(3), 224–274 (2001) [35] Fisler, K., Krishnamurthi, S., Meyerovich, L.A., Tschantz, M.C.: Verifica- tion and change-impact analysis of access-control policies. In: Proceedings of the 27th international conference on Software engineering. pp. 196–205. ACM (2005) [36] Fosdick, L.D., Osterweil, L.J.: Data flow analysis in software reliability. In: Engineering of Software, pp. 49–85. Springer (2011) [37] Gouglidis, A., Hu, V.C., Busby, J.S., Hutchison, D.: Verification of re- silience policies that assist attribute based access control. In: Proceedings of the 2nd ACM Workshop on Attribute-Based Access Control. pp. 43–52 (2017) [38] Haldar, V., Chandra, D., Franz, M.: Dynamic taint propagation for Java. In: 21st Annual Computer Security Applications Conference (ACSAC’05). pp. 9–pp. IEEE (2005) 116 [39] Hall, A.A., Wright, C.S.: Data Security: A review of major security breaches between 2014 and 2018. Federation of Business Disciplines Journal pp. 50–63 (2018) [40] Hansen, F., Oleshchuk, V.: Conformance checking of RBAC policy and its implementation. In: International Conference on Information Security Practice and Experience. pp. 144–155. Springer (2005) [41] Hu, C.T., Ferraiolo, D.F., Kuhn, D.R., Schnitzer, A., Sandlin, K., Miller, R., Scarfone, K.: Guide to Attribute Based Access Control (ABAC) Defi- nition and Considerations [includes updates as of 02-25-2019]. Tech. rep. (2019) [42] Hu, V.: Attribute based access control (ABAC) definition and considera- tions. Tech. rep., National Institute of Standards and Technology (2014) [43] Hu, V.C., Ferraiolo, D., Kuhn, D.R.: Assessment of access control sys- tems. US Department of Commerce, National Institute of Standards and Technology (2006) [44] Hu, V.C., Ferraiolo, D., Kuhn, R., Friedman, A.R., Lang, A.J., Cogdell, M.M., Schnitzer, A., Sandlin, K., Miller, R., Scarfone, K., et al.: Guide to attribute based access control (abac) definition and considerations (draft). NIST special publication 800(162) (2013) [45] Hu, V.C., Kuhn, D.R., Ferraiolo, D.F., Voas, J.: Attribute-based access control. Computer 48(2), 85–88 (2015) [46] Hu, V.C., Kuhn, R., Yaga, D.: Verification and test methods for access control policies/models. NIST Special Publication 800, 192 (2017) [47] Hughes, G., Bultan, T.: Automated verification of access control policies using a sat solver. International Journal on Software Tools for Technology Transfer (STTT) 10(6), 503–520 (2008) [48] Idani, A.: Model driven secure web applications: the SeWAT platform. In: Proceedings of the Fifth European Conference on the Engineering of Computer-Based Systems. p. 3. ACM (2017) [49] Jha, S., Sural, S., Atluri, V., Vaidya, J.: Specification and verification of separation of duty constraints in attribute-based access control. IEEE Transactions on Information Forensics and Security 13(4), 897–911 (2018) [50] Jin, X., Krishnan, R., Sandhu, R.: A unified attribute-based access control model covering DAC, MAC and RBAC. In: IFIP Annual Conference on Data and Applications Security and Privacy. pp. 41–55. Springer (2012) [51] Kauser, S., Rahman, A., Khan, A.M., Ahmad, T.: Attribute-Based Ac- cess Control in Web Applications. In: Applications of Artificial Intelligence Techniques in Engineering, pp. 385–393. Springer (2019) 117 [52] Kumar, I.R., SreeRam, N., Tech, J.R.K.M.: Enhancing The Development Life Cycle To Produce Secure Software (2012) [53] Lam, M.S., Martin, M., Livshits, B., Whaley, J.: Securing web applications with static and dynamic information flow tracking. In: Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics- based program manipulation. pp. 3–12 (2008) [54] Li, X., Xue, Y.: A survey on web application security. Nashville, TN USA 25(5), 1–14 (2011) [55] Li, X., Xue, Y.: Block: a black-box approach for detection of state viola- tion attacks towards web applications. In: Proceedings of the 27th Annual Computer Security Applications Conference. pp. 247–256 (2011) [56] Livshits, V.B., Lam, M.S.: Finding Security Vulnerabilities in Java Appli- cations with Static Analysis. In: USENIX Security Symposium. vol. 14, pp. 18–18 (2005) [57] Lodderstedt, T., Basin, D., Doser, J.: SecureUML: A UML-based modeling language for model-driven security. In: International Conference on the Unified Modeling Language. pp. 426–441. Springer (2002) [58] Louridas, P.: Static code analysis. IEEE Software 23(4), 58–61 (2006) [59] Ma, H., Xie, C.: A Design of Multi-level Structure Security Architecture on Database Ap-plication System. Open Automation and Control Systems Journal 6, 1510–1514 (2014) [60] MacIntyre, C.R., Engells, T.E., Scotch, M., Heslop, D.J., Gumel, A.B., Poste, G., Chen, X., Herche, W., Steinho¨fel, K., Lim, S., et al.: Converging and emerging threats to health security. Environment Systems and Deci- sions 38(2), 198–207 (2018) [61] Martin, E., Hwang, J., Xie, T., Hu, V.: Assessing quality of policy prop- erties in verification of access control policies. In: 2008 Annual Computer Security Applications Conference (ACSAC). pp. 163–172. IEEE (2008) [62] Martínez, S., Cosentino, V., Cabot, J.: Model-based analysis of Java EE web security configurations. In: 2016 IEEE/ACM 8th International Work- shop on Modeling in Software Engineering (MiSE). pp. 55–61. IEEE (2016) [63] Matulevicˇius, R., Dumas, M.: A Comparison of SecureUML and UMLsec for Rolebased Access Control. In: Proceedings of the 9th Conference on Databases and Information Systems. pp. 171–185 (2010) [64] McGraw, G.: Software security: building security in, vol. 1. Addison-Wesley Professional (2006) [65] Mead, N.R., Allen, J.H., Barnum, S., Ellison, R.J., McGraw, G.: Software Security Engineering: A Guide for Project Managers. Addison-Wesley Pro- fessional (2004) 118 [66] Meng, N., Nagy, S., Yao, D., Zhuang, W., Arango-Argoty, G.: Secure coding practices in java: Challenges and vulnerabilities. In: 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE). pp. 372–383. IEEE (2018) [67] Mogensen, T.Æ.: Basics of compiler design. Torben Ægidius Mogensen (2009) [68] Mularien, P.: Spring Security 3. Packt Publishing Ltd (2010) [69] Murthy, P.K.: Constructing a control flow graph for a software program (Feb 3 2015), uS Patent 8,949,811 [70] Nabil, D., Slimani, H., Nacer, H., Aissani, D., Bey, K.B.: ABAC Conceptual Graph Model for Composite Web Services. In: 2018 IEEE 5th International Congress on Information Science and Technology (CiSt). pp. 36–41. IEEE (2018) [71] Nadji, Y., Saxena, P., Song, D.: Document Structure Integrity: A Robust Basis for Cross-site Scripting Defense. In: NDSS. vol. 20 (2009) [72] Parducci, B., Lockhart, H., Rissanen, E.: Extensible access control markup language (XACML) version 3.0. OASIS Standard pp. 1–154 (2013) [73] Patel, R.R.: Finding Security Vulnerabilities in Java Application with Static Taint Analysis. Ph.D. thesis, Texas A&M University-Kingsville (2018) [74] Perrin, C.: The CIA triad. Dostopno na: techrepublic. com/blog/security/the-cia-triad/488 (2008) [75] Pistoia, M., Chandra, S., Fink, S.J., Yahav, E.: A survey of static analysis methods for identifying security vulnerabilities in software systems. IBM Systems Journal 46(2), 265–288 (2007) [76] Pistoia, M., Fink, S.J., Flynn, R.J., Yahav, E.: When role models have flaws: Static validation of enterprise security policies. In: 29th International Conference on Software Engineering (ICSE’07). pp. 478–488. IEEE (2007) [77] Principe, M., Yoon, D.: A Web Application Using MVC Framework. In: Proceedings of the International Conference on e-Learning, e-Business, En- terprise Information Systems, and e-Government (EEE). p. 10 (2015) [78] Qamar, N., Faber, J., Ledru, Y., Liu, Z.: Automated reviewing of healthcare security policies. In: International Symposium on Foundations of Health Informatics Engineering and Systems. pp. 176–193. Springer (2012) [79] Qamar, N., Ledru, Y., Idani, A.: Validation of security-design models using Z. In: International Conference on Formal Engineering Methods. pp. 259– 274. Springer (2011) 119 [80] Rashid, F.Y.: Library misuse exposes leading java platforms to at- tack (2017), https://www.infoworld.com/article/3003197/security/ library-misuse-exposes-leading-java-platforms-to-attack.html [81] Robertson, W.K., Vigna, G.: Static Enforcement of Web Application In- tegrity Through Strong Typing. In: USENIX Security Symposium. vol. 9, pp. 283–298 (2009) [82] Samuel, M., Saxena, P., Song, D.: Context-sensitive auto-sanitization in web templating languages using type qualifiers. In: Proceedings of the 18th ACM conference on Computer and communications security. pp. 587–600 (2011) [83] Sandhu, R., Coyne, E., Feinstein, H., Role-Based, C.Y.: Access Control Models. IEEE computer 29(2), 38–47 (2013) [84] Saxena, P., Hanna, S., Poosankam, P., Song, D.: FLAX: Systematic Dis- covery of Client-side Validation Vulnerabilities in Rich Web Applications. In: NDss (2010) [85] Saxena, P., Molnar, D., Livshits, B.: SCRIPTGARD: automatic context- sensitive sanitization for large-scale legacy web applications. In: Proceed- ings of the 18th ACM conference on Computer and communications secu- rity. pp. 601–614 (2011) [86] Scarioni, C.: Pro Spring Security. Apress (2013) [87] Sergeev, A.: Role Based Access Control as SecureUML Model in Web Ap- plications Development with Spring Security. Ph.D. thesis, Master thesis, University of Tartu (2016) [88] Sergeev, A., Matulevicius, R.: An Approach to Capture Role-Based Access Control Models from Spring Web Applications. In: 2017 IEEE 21st Inter- national Enterprise Distributed Object Computing Conference (EDOC). pp. 159–164. IEEE (2017) [89] Sharma, N.K., Joshi, A.: Representing attribute based access control poli- cies in owl. In: 2016 IEEE Tenth International Conference on Semantic Computing (ICSC). pp. 333–336. IEEE (2016) [90] Shklar, L., Rosen, R.: Web application architecture. John Wiley & Sons (2009) [91] Shrestha, N., Alsadoon, A., Prasad, P., Hourany, L., Elchouemi, A.: En- hanced e-health framework for security and privacy in healthcare system. In: 2016 Sixth International Conference on Digital Information Processing and Communications (ICDIPC). pp. 75–79. IEEE (2016) [92] Shu, C.c., Yang, E.Y., Arenas, A.E.: Detecting conflicts in abac policies with rule-reduction and binary-search techniques. In: 2009 IEEE Interna- tional Symposium on Policies for Distributed Systems and Networks. pp. 182–185. IEEE (2009) 120 [93] Smelik, R., Rensink, A., Kastenberg, H.: Specification and construction of control flow semantics. In: Visual Languages and Human-Centric Comput- ing, 2006. VL/HCC 2006. IEEE Symposium on. pp. 65–72. IEEE (2006) [94] So¨derberg, E., Ekman, T., Hedin, G., Magnusson, E.: Extensible intrapro- cedural flow analysis at the abstract syntax tree level. Science of Computer Programming 78(10), 1809–1827 (2013) [95] Sohr, K., Drouineaud, M., Ahn, G.J.: Formal specification of role-based security policies for clinical information systems. In: Proceedings of the 2005 ACM symposium on Applied computing. pp. 332–339 (2005) [96] for Standardization, I.O.: Information Technology, Z Formal Specification Notation: Syntax, Type System and Semantics. ISO/IEC (2002) [97] Sui, L., Dietrich, J., Tahir, A., Fourtounis, G.: On the recall of static call graph construction in practice. In: 2020 IEEE/ACM 42nd International Conference on Software Engineering (ICSE). pp. 1049–1060. IEEE (2020) [98] Sun, F., Xu, L., Su, Z.: Static Detection of Access Control Vulnerabilities in Web Applications. In: USENIX Security Symposium. vol. 64 (2011) [99] Symantec, C.: Internet security threat report 2019 (2014) [100] Touseef, P., Ashraf, M.A., Rafiq, A.: Analysis of Risks against Web Appli- cations in MVC. NFC IEFR Journal of Engineering and Scientific Research 5 (2017) [101] Ubale Swapnaja, A., Modani Dattatray, G., Apte Sulabha, S.: Analysis of dac mac rbac access control based models for security. International Journal of Computer Applications 104(5), 6–13 (2014) [102] Vaidya, R.: Cyber security breaches survey 2019 (2019) [103] Wang, L., Wijesekera, D., Jajodia, S.: A logic-based framework for attribute based access control. In: Proceedings of the 2004 ACM workshop on Formal methods in security engineering. pp. 45–55 (2004) [104] Wang, T., Li, W.h., Liu, Z.: RBAC Permission Consistency Static Analysis Framework. In: 2010 International Conference on Multimedia Information Networking and Security. pp. 506–510. IEEE (2010) [105] Weinberger, J., Saxena, P., Akhawe, D., Finifter, M., Shin, R., Song, D.: A systematic analysis of XSS sanitization in web application frameworks. In: European Symposium on Research in Computer Security. pp. 150–171. Springer (2011) [106] Wilander, J., et al.: Pattern matching security properties of code using dependence graphs. In: Proceedings of the First International Workshop on Code Based Software Security Assessments. Citeseer (2005) 121 [107] Wo¨gerer, W.: A survey of static program analysis techniques. Tech. rep., Tech. rep., Technische Universita¨t Wien (2005) [108] Xu, D., Zhang, Y.: Specification and analysis of attribute-based access con- trol policies: An overview. In: 2014 IEEE Eighth International Conference on Software Security and Reliability-Companion. pp. 41–49. IEEE (2014) 122