ĐẠI HỌC QUỐC GIA TP. HỒ CHÍ MINH TRƯỜNG ĐẠI HỌC BÁCH KHOA --------------------------------------- ĐINH KIM QUỐC KHẢI AUTOMATED SECURITY ANALYSIS OF ADMINISTRATIVE ROLE-BASED ACCESS CONTROL POLICIES WITH CONTEXTUAL INFORMATION LUẬN VĂN THẠC SĨ TP. HỒ CHÍ MINH, tháng 12 năm 2017 ĐẠI HỌC QUỐC GIA TP. HỒ CHÍ MINH TRƯỜNG ĐẠI HỌC BÁCH KHOA --------------------------------------- ĐINH KIM QUỐC KHẢI AUTOMATED SECURITY ANALYSIS OF ADMINISTRATIVE ROLE-BASED ACCESS CONTROL POLICIES WITH CONTEXTUAL INFORMATION Chuyên ngành: KHOA HỌC MÁY TÍNH MÃ NGÀNH: 60.01 LUẬN VĂN THẠC SĨ TS.TRƯƠNG TUẤN ANH TP.
HỒ CHÍ MINH, tháng 12 năm 2017 CÔNG TRÌNH ĐƯỢC HOÀN THÀNH TẠI TRƯỜNG ĐẠI HỌC BÁCH KHOA –ĐHQG -HCM Cán bộ hướng dẫn khoa học : TS. Trương Tuấn Anh (Ghi rõ họ, tên, học hàm, học vị và chữ ký) Cán bộ chấm nhận xét 1 : TS. Phan Trọng Nhân (Ghi rõ họ, tên, học hàm, học vị và chữ ký) Cán bộ chấm nhận xét 2 : PGS. Trần Minh Triết (Ghi rõ họ, tên, học hàm, học vị và chữ ký) Luận văn thạc sĩ được bảo vệ tại Trường Đại học Bách Khoa, ĐHQG Tp.
HCM ngày 28 tháng 12 năm 2017 Thành phần Hội đồng đánh giá luận văn thạc sĩ gồm: (Ghi rõ họ, tên, học hàm, học vị của Hội đồng chấm bảo vệ luận văn thạc sĩ) 1. Lê Hồng Trang 3. Phan Trọng Nhân 4. Trần Minh Triết 5.
Nguyễn Văn Vũ Xác nhận của Chủ tịch Hội đồng đánh giá LV và Trưởng Khoa quản lý chuyên ngành sau khi luận văn đã được sửa chữa (nếu có). CHỦ TỊCH HỘI ĐỒNG TRƯỞNG KHOA KH&KTMT ĐẠI HỌC QUỐC GIA TP.HCM CỘNG HÒA XÃ HỘI CHỦ NGHĨA VIỆT NAM Độc lập - Tự do - Hạnh phúc TRƯỜNG ĐẠI HỌC BÁCH KHOA NHIỆM VỤ LUẬN VĂN THẠC SĨ Họ tên học viên: Đinh Kim Quốc Khải MSHV: 7140239 Ngày, tháng, năm sinh: 19/05/1991 Nơi sinh: TP.HCM Chuyên ngành: Khoa học máy tính TÊN ĐỀ TÀI: Phân tích tự động thuộc tính bảo mật cho mô hình điều khiển truy xuất không- thời gian (Automated security analysis of administrative role-based access control policies with contextual information) I. NHIỆM VỤ VÀ NỘI DUNG: - Nghiên cứu, tìm hiểu các mô hình điều khiển truy xuất, đặc biệt là RBAC và mô hình quản trị ARBAC của nó - Nghiên cứu mô hình mở rộng của RBAC có các thông tin ngữ cảnh như không và thời gian - Tìm hiểu bài toán phân tích user-role reachability problem cho mô hình mở rông RBAC có các thông tin ngữ cảnh - Thiết kế công cụ phân tích tự động giải quyết bài toán user-role reachability - Thiết kế các heuristics để tăng tốc độ phân tích II. NGÀY GIAO NHIỆM VỤ : (Ghi theo trong QĐ giao đề tài) 03/07/2017 III.
NGÀY HOÀN THÀNH NHIỆM VỤ: (Ghi theo trong QĐ giao đề tài) 01/12/2017 IV.CÁN BỘ HƯỚNG DẪN (Ghi rõ học hàm, học vị, họ, tên): TS. Trương Tuấn Anh Tp. CÁN BỘ HƯỚNG DẪN TRƯỞNG KHOA (Họ tên và chữ ký) (Họ tên và chữ ký) TS. Trương Tuấn Anh LỜI CẢM ƠN Luận văn thạc sĩ khoa khoa học và kỹ thuật máy tính với đề tài “Phân tích tự động thuộc tính bảo mật cho mô hình điều khiển truy xuất không- thời gian” là kết quả của quá trình cố gắng không ngừng của bản thân và được sự giúp đỡ, động viên khích lệ của các thầy, bạn bè đồng nghiệp và người thân.
Qua trang viết này tác giả xin gửi lời cảm ơn tới những người đã giúp đỡ tôi trong thời gian học tập - nghiên cứu khoa học vừa qua. Tôi xin tỏ lòng kính trọng và biết ơn sâu sắc đối với thầy giáo TS. Trương Tuấn Anh đã trực tiếp tận tình hướng dẫn cũng như cung cấp tài liệu thông tin khoa học cần thiết cho luận văn này. Xin chân thành cảm ơn Lãnh đạo trường Đại học Bách Khoa Tp.HCM đã tạo điều kiện cho tôi hoàn thành tốt công việc nghiên cứu khoa học của mình.
Cuối cùng tôi xin chân thành cảm ơn đồng nghiệp, đơn vị công tác đã giúp đỡ tôi trong quá trình học tập và thực hiện Luận văn. Đinh Kim Quốc Khải TÓM TẮT LUẬN VĂN Mô hình điều khiển truy xuất trên cơ sở vai trò (RBAC - Role-based Access Control) là một mô hình được quan tâm và sử dụng rộng rãi trong doanh nghiệp để giúp quản lý và ngăn chặn người dung truy cập trái phép các tài nguyên trong hệ thống. Nhiều đề tài đã được thực hiện và nghiên cứu phát triển mở rông mô hình RBAC đáp ứng các nhu cầu bảo mật cao hơn khi số lượng người dùng và người quản trị càng lớn. Mỗi nhà quản trị (admin) sẽ thay đổi 1 phần trong các policy.
Tuy nhiên, sự kết hợp giữa những thay đổi của các nhà quản trị này có thể dẫn policy đến trạng thái vi phạm thuộc tính bảo mật của hệ thống. Vì vây, phải có giải pháp để kiểm tra tất cả sự thay đổi này để xem thử các lỗ hổng bảo mật (trạng thái thuộc tính bảo mật bị vi phạm) có xảy ra hay không. Một trong các mô hình đó là mô hình quản trị điều khiển truy xuất trên cơ sở vai trò ARBAC97 (Administrative Role-based Access Control) để quản trị quyền của những người dùng có quyền quản trị trên mô hình RBAC. Để đáp ứng nhu cầu kiểm soát truy cập trong các hệ thống quan trọng hiện nay, nhiều mô hình điều khiển truy xuất có ràng buộc về không gian và thời gian đã được áp dụng dựa trên mô hình RBAC như Spatial-Temporal Role-Based Access Control (STRBAC).
Tuy nhiên, các nhà quản trị của mô hình STRBAC cũng có thể thực hiện thay đổi 1 phần trong các policy đó mà sự kết hợp giữa những thay đổi của các nhà quản trị này có thể dẫn policy đến trạng thái vi phạm thuộc tính bảo mật của hệ thống. Tuy nhiên, hiện nay vẫn chưa có các nghiên cứu việc tìm giải pháp cho mô hình biến thể mở rộng này. Trong dề tài này, chúng tôi tập trung chủ yếu vào các giải pháp phân tích bảo mật cho mô hình quản lý truy xuất Spatial Temporal RBAC (STRBAC). và minh họa kỹ thuật phân tích để phát hiện và ngăn chặn các vấn đề bảo mật của mô hình kiểm soát truy cập này bằng cách sử dụng logic vị từ và kỹ thuật kiểm định mô hình.
Các thực nghiệm của chúng tôi xác nhận tính đúng đắn của các giải pháp đề xuất này trong việc phân tích tập chính sách hữu hạn mà không biết trước về số người dùng trong hệ thống. ABSTRACT Role-based Access Control (RBAC) has made great attention in the security community and is widely deployed in the enterprise as a major tool to manage security and restrict system access to unauthorized users. As the RBAC model evolves to meet enterprise requirements, the RBAC policies will become complex and need to be managed by multiple collaborative administrators. The collaborative administrator may interact unintendedly with the policies, creates the undesired effect to the security requirements of the enterprise.
Consequently, researchers have studied various safety analyzing techniques that are useful to prevent this issues in RBAC, especially with the Administrative Role-Based Access Control (ARBAC97). For critical applications, several extensions of RBAC, such as Spatial- Temporal Role-Based Access Control (STRBAC), are being adopted in recent years to enhance the security of an application on authorization with contextual information such as time and space. The features, which proposed in STRBAC for collaborative administrators, may interact in subtle ways that violate the original security requirements. However, the analysis of it has not been considered in the literature.
In this research, we consider the security analysis technique for the extension of STRBAC, named Administrative STRBAC (ASTRBAC), and illustrate the safety analysis technique to detect and prevent the security problem of this access control model. This technique leverages First-Order Logic and Symbolic Model Checking (SMT) by translating the policies to decidable reachability problem, which are essential to understand the security policies and inform policies designer using this model to take appropriate actions. Our extensive experimental evaluation confirms the correctness of our proposed solutions, which supports finite ASTRBAC policies analysis without prior knowledge about the number of users in the system. LỜI CAM ĐOAN Tôi xin cam đoan đây là công trình nghiên cứu khoa học độc lập của riêng tôi.
Các số liệu sử dụng phân tích trong luận án có nguồn gốc rõ ràng, đã công bố theo đúng quy định. Các kết quả nghiên cứu trong luận án do tôi tự tìm hiểu, phân tích một cách trung thực, khách quan và phù hợp với thực tiễn của Việt Nam. Các kết quả này chưa từng được công bố trong bất kỳ nghiên cứu nào khác. Đinh Kim Quốc Khải ACRONYM LIST ARBAC Administrative Role-Based Access Control ASTRBAC Administrative Spatial-Temporal Role-Based Acesss Control ASASPSPCAETIME Automated Symbolic Analysis of Security Policies tool with SPACE and TIME BR Backward Reachability BSR Bernays-Schonfinkel-Ramsey DAC Discretionary Access Control MAC Mandatory Access Control PA Permission Assignment PE Permission Extents RE Role Extents RBAC Role-based Access Control STRBAC Spatial-Temporal Role-Based Access Control SMT Symbolic Model Checking UA User Assignment LIST OF FIGURES Fig.
3: Policies P1 is changed to P2. 4: Executing rule 2 on policies P2. 9: Our technique to solve the reachability problem for ASTRBAC. 10: ASASPSPACETIME with heuristics.
11: Our average run time at different locations. 12: Our average runtime with different time slots. 66 LIST OF TABLES Table 1: Our first experimental results. 64 Table 2: Our second experimental results with different locations.
65 Table 3: Our second experimental results with different time slots. 65 Table 4: Our third experiments with heuristics. Objectives of this study. Scope of this study.
Purpose of this study. RBAC and STRBAC. Role-Based Access Control (RBAC). Administrative Role-Based Access Control (ARBAC).
Spatial-Temporal Role-based Access Control (STRBAC). Administrative Spatial-Temporal Role-based Access Control (ASTRBAC). User-role reachability for STRBAC. Related Works And Materials.
AUTOMATED ANALYSIS FOR ASTRBAC. Implementing the Translator. Optimizing the performance. Combining Forwarding and Backwarding.
Combining Complement Actions. Removing Duality Actions. Separating complex goal. Applying all heuristics.
Evaluations ASASPSPACETIME with heuristics. RESEARCH PROBLEMS Role-based access control (RBAC) [4][5] is gaining more attention in protecting enterprise data against malicious users and criminals. Access control [1] is essential to mediate every request to enterprise resources and decide whether to approve or reject each request. Manipulating these requests requires access control policies to define higher level rules to regulate and control who and what kind of permissions can access specific resources.
Although many access control models have been developed like Discretionary Access Control (DAC) [2] or Mandatory Access Control (MAC)[3], only RBAC achieves awareness against users and vendors due to its benefits for organizations which separates responsibilities in a system where multiple roles are fulfilled. In RBAC, the access permissions are associated with roles, and users must be made members of appropriate roles to grant access. Using Principle of Least Privilege and Separation of Duties, no one can have discretionary access to enterprise resources to perform malicious activities since no standalone individual has all permissions needed for an important operation. RBAC simplifies management of authorization and flexible in specifying and enforcing policies which can be added or removed for a particular role as needed.