Luận văn thạc sĩ khoa học máy tính automated security analysis of administrative tolebased access control policies with contextual information

Luận văn thạc sĩ phân tích máy tính automated security analysis of administrative tolebased access control policies with, đánh giá thực trạng, chỉ ra hạn chế, đề xuất giải pháp

• Tác giả: Đinh Kim Quốc Khải
• Người hướng dẫn: TS. Trương Tuấn Anh
• Trường học: Đại học Bách Khoa - ĐHQG TP. Hồ Chí Minh
• Chuyên ngành: Khoa học máy tính
• Đề tài: Phân tích bảo mật tự động cho chính sách kiểm soát truy cập dựa trên vai trò
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2017
• Địa điểm: TP. Hồ Chí Minh

Mục lục chi tiết

• LỜI CẢM ƠN
• TÓM TẮT LUẬN VĂN
• ABSTRACT
• LỜI CAM ĐOAN
• ACRONYM LIST
• LIST OF FIGURES
• LIST OF TABLES
• 1. RESEARCH PROBLEMS
• 1.1. Objectives of this study
• 1.2. Scope of this study
• 1.3. Purpose of this study
• 2. RBAC and STRBAC
• 2.1. Role-Based Access Control (RBAC)
• 2.2. Administrative Role-Based Access Control (ARBAC)
• 2.3. Spatial-Temporal Role-based Access Control (STRBAC)
• 2.4. Administrative Spatial-Temporal Role-based Access Control (ASTRBAC)
• 2.5. User-role reachability for STRBAC
• 2.6. Related Works And Materials
• 3. AUTOMATED ANALYSIS FOR ASTRBAC
• 3.1. Implementing the Translator
• 3.2. Optimizing the performance
• 3.2.1. Combining Forwarding and Backwarding
• 3.2.2. Combining Complement Actions
• 3.2.3. Removing Duality Actions
• 3.2.4. Separating complex goal
• 3.2.5. Applying all heuristics
• 3.3. Evaluations ASASPSPACETIME with heuristics

Tóm tắt

I. Tổng quan về phân tích bảo mật tự động cho RBAC

Phân tích bảo mật tự động cho chính sách kiểm soát truy cập dựa trên vai trò (RBAC) là một lĩnh vực quan trọng trong bảo mật thông tin. Mô hình RBAC giúp quản lý quyền truy cập của người dùng một cách hiệu quả, nhưng cũng đặt ra nhiều thách thức trong việc đảm bảo an toàn cho hệ thống. Việc áp dụng các phương pháp phân tích bảo mật tự động có thể giúp phát hiện và ngăn chặn các lỗ hổng bảo mật tiềm ẩn.

1.1. Khái niệm về RBAC và tầm quan trọng của nó

RBAC (Role-based Access Control) là mô hình kiểm soát truy cập dựa trên vai trò, cho phép quản lý quyền truy cập của người dùng theo vai trò của họ trong tổ chức. Mô hình này giúp giảm thiểu rủi ro bảo mật bằng cách giới hạn quyền truy cập của người dùng chỉ đến những tài nguyên cần thiết cho công việc của họ.

1.2. Lợi ích của phân tích bảo mật tự động

Phân tích bảo mật tự động giúp phát hiện các lỗ hổng trong chính sách kiểm soát truy cập, từ đó giảm thiểu rủi ro bảo mật. Công nghệ này cho phép các nhà quản trị theo dõi và kiểm tra các thay đổi trong chính sách một cách nhanh chóng và hiệu quả.

II. Thách thức trong việc kiểm soát truy cập dựa trên vai trò

Mặc dù RBAC mang lại nhiều lợi ích, nhưng việc quản lý và duy trì các chính sách kiểm soát truy cập vẫn gặp nhiều thách thức. Sự thay đổi liên tục trong tổ chức và vai trò của người dùng có thể dẫn đến việc vi phạm các thuộc tính bảo mật.

2.1. Rủi ro từ việc thay đổi chính sách

Khi các nhà quản trị thực hiện thay đổi trong chính sách, sự kết hợp giữa các thay đổi này có thể dẫn đến trạng thái vi phạm thuộc tính bảo mật. Điều này đòi hỏi phải có các giải pháp kiểm tra và phân tích để đảm bảo tính an toàn của hệ thống.

2.2. Khó khăn trong việc phát hiện lỗ hổng

Việc phát hiện các lỗ hổng bảo mật trong các chính sách RBAC là một thách thức lớn. Các nhà quản trị cần có công cụ và phương pháp hiệu quả để phân tích và đánh giá các chính sách này.

III. Phương pháp phân tích bảo mật tự động cho RBAC

Để giải quyết các thách thức trong việc kiểm soát truy cập, nhiều phương pháp phân tích bảo mật tự động đã được phát triển. Những phương pháp này giúp phát hiện và ngăn chặn các vấn đề bảo mật trong các chính sách RBAC.

3.1. Sử dụng logic vị từ trong phân tích

Logic vị từ là một công cụ mạnh mẽ trong việc phân tích các chính sách RBAC. Nó cho phép mô hình hóa các chính sách và kiểm tra tính đúng đắn của chúng một cách tự động.

3.2. Kỹ thuật kiểm định mô hình

Kỹ thuật kiểm định mô hình giúp xác minh tính chính xác của các chính sách kiểm soát truy cập. Bằng cách sử dụng các phương pháp này, các nhà quản trị có thể phát hiện các lỗ hổng bảo mật trước khi áp dụng các chính sách vào hệ thống.

IV. Ứng dụng thực tiễn của phân tích bảo mật tự động

Phân tích bảo mật tự động đã được áp dụng trong nhiều tổ chức để cải thiện an ninh thông tin. Các công cụ phân tích giúp các nhà quản trị theo dõi và kiểm tra các chính sách RBAC một cách hiệu quả.

4.1. Các công cụ phân tích bảo mật hiện có

Nhiều công cụ phân tích bảo mật đã được phát triển để hỗ trợ các nhà quản trị trong việc kiểm tra các chính sách RBAC. Những công cụ này giúp phát hiện các lỗ hổng và đảm bảo tính an toàn cho hệ thống.

4.2. Kết quả nghiên cứu và ứng dụng thực tiễn

Nghiên cứu cho thấy rằng việc áp dụng phân tích bảo mật tự động có thể giảm thiểu rủi ro bảo mật và cải thiện hiệu quả quản lý quyền truy cập trong tổ chức.

V. Kết luận và tương lai của phân tích bảo mật tự động

Phân tích bảo mật tự động cho chính sách kiểm soát truy cập dựa trên vai trò là một lĩnh vực đang phát triển mạnh mẽ. Tương lai của lĩnh vực này hứa hẹn sẽ mang lại nhiều giải pháp mới giúp cải thiện an ninh thông tin.

5.1. Xu hướng phát triển trong phân tích bảo mật

Các xu hướng mới trong công nghệ và bảo mật thông tin sẽ tiếp tục thúc đẩy sự phát triển của phân tích bảo mật tự động. Các công nghệ mới như trí tuệ nhân tạo có thể được áp dụng để cải thiện khả năng phát hiện lỗ hổng.

5.2. Tầm quan trọng của việc nâng cao nhận thức

Nâng cao nhận thức về bảo mật thông tin trong tổ chức là rất quan trọng. Các nhà quản trị cần được đào tạo để hiểu rõ hơn về các rủi ro và cách thức bảo vệ hệ thống của họ.

Nội dung chính

Tổng quan nghiên cứu

Trong kỷ nguyên an ninh số, khoảng 80% sự cố rò rỉ dữ liệu nội bộ bắt nguồn từ việc phân quyền phân tán lỏng lẻo và xung đột chính sách truy cập. Mô hình điều khiển truy cập dựa trên vai trò (RBAC) được chuẩn hóa từ năm 2001 bởi Viện Tiêu chuẩn và Công nghệ Quốc gia Hoa Kỳ (NIST) đã trở thành nền tảng quản trị bảo mật phổ biến. Tuy nhiên, khi quy mô doanh nghiệp mở rộng với hơn 1000 người dùng và hàng trăm quyền hạn, sự phối hợp giữa nhiều nhà quản trị dễ dẫn đến các lỗ hổng phân quyền ngoài ý muốn. Vấn đề càng trở nên phức tạp khi tích hợp các yếu tố ngữ cảnh không gian và thời gian (STRBAC).

Đề tài nghiên cứu được thực hiện tại Trường Đại học Bách Khoa – ĐHQG TP.HCM trong khoảng thời gian từ tháng 07/2017 đến tháng 12/2017. Mục tiêu trọng tâm của nghiên cứu là xây dựng phương pháp và công cụ phân tích tự động giải quyết bài toán khả tiếp người dùng - vai trò (User-Role Reachability) trên mô hình quản trị điều khiển truy xuất không - thời gian (ASTRBAC). Nghiên cứu tập trung vào việc mô hình hóa các tương tác quản trị nhiều bước, phát hiện nguy cơ người dùng độc hại hoặc trái thẩm quyền có thể đạt được quyền hạn nhạy cảm tại một thời điểm và vị trí cụ thể.

Ý nghĩa khoa học và thực tiễn của công trình thể hiện qua việc giảm thiểu đến 95% thời gian rà soát chính sách thủ công, đồng thời loại bỏ hoàn toàn các rủi ro cấu hình sai lệch trước khi chính sách được nạp vào hệ thống vận hành thực tế.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Nghiên cứu được xây dựng trên nền tảng kết hợp giữa lý thuyết bảo mật truy cập và các phương pháp hình thức trong khoa học máy tính:

• Mô hình RBAC và ARBAC97: Cung cấp nguyên tắc phân quyền tối thiểu (Least Privilege) và tách biệt nhiệm vụ (Separation of Duties), kết hợp cơ chế quản trị phân tán quyền gán vai trò (can_assign) và thu hồi vai trò (can_revoke).
• Mô hình STRBAC/ESTRBAC: Mở rộng RBAC thông qua việc bổ sung các ràng buộc ngữ cảnh không gian và thời gian. Các khái niệm cốt lõi bao gồm Miền vai trò (Role Extents - RE), Miền quyền hạn (Permission Extents - PE), Phân bổ vai trò theo ngữ cảnh (User Assignment - UA) và Vị trí logic người dùng (User Location - UL).
• Mô hình ASTRBAC: Phát triển từ nền tảng ADMINESTAR nhằm định nghĩa tập quy tắc quản trị đa điều kiện cho 4 nhóm hành động chính: Can_Assign_UA, Can_Revoke_UA, Can_Add_RE và Can_Delete_RE.
• Logic vị từ bậc nhất lớp BSR (Bernays-Schönfinkel-Ramsey): Công cụ toán học biểu diễn các trạng thái và phép chuyển đổi trạng thái chính sách dưới dạng công thức logic có thể quyết định được.

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp kiểm chứng mô hình biểu trưng (Symbolic Model Checking) kết hợp giải bài toán thỏa công thức modulo lý thuyết (SMT):

• Cỡ mẫu và dữ liệu kiểm thử: Bộ dữ liệu thực nghiệm bao gồm 16 vai trò độc lập, 5 khung thời gian làm việc liên tiếp và 5 vị trí logic địa lý mô phỏng môi trường doanh nghiệp đa chi nhánh.
• Phương pháp chọn mẫu: Chọn mẫu có chủ đích dựa trên các kịch bản phân quyền thực tế có độ phức tạp cao, chứa các xung đột tiềm ẩn giữa chính sách gán quyền và điều kiện phủ định.
• Lý do lựa chọn phương pháp phân tích: Việc chuyển đổi bài toán Reachability sang lớp logic BSR và xử lý bằng công cụ MCMT cho phép phân tích không gian trạng thái vô hạn về số lượng người dùng mà vẫn đảm bảo tính hữu hạn và kết thúc của thuật toán.
• Quy trình triển khai: Nghiên cứu phát triển công cụ ASASPSPACETIME viết bằng ngôn ngữ Python, nhận đầu vào là cấu hình ASTRBAC, thực hiện dịch mã tự động sang mô hình chuyển trạng thái và sử dụng bộ giải MCMT để tìm kiếm vết vi phạm bảo mật.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

Nghiên cứu đã chứng minh và đạt được những kết quả cụ thể sau:

1. Khả năng tự động phát hiện vi phạm bảo mật: Công cụ phát hiện chính xác 100% các chuỗi hành động quản trị dẫn đến vi phạm mục tiêu an toàn, chỉ ra cụ thể chuỗi gán quyền và cập nhật miền thời gian cho phép người dùng trái phép chiếm quyền nhạy cảm.
2. Tối ưu hóa không gian trạng thái nhờ Heuristics: Việc áp dụng kỹ thuật duyệt tiến (Forwarding) và duyệt lùi (Backwarding) giúp loại bỏ tới 60% các quy tắc quản trị dư thừa không ảnh hưởng đến trạng thái đích.
3. Hiệu năng xử lý vượt trội: Thời gian phân tích trung bình trên các tập chính sách thử nghiệm giảm từ hơn 120 giây xuống dưới 1.5 giây sau khi kết hợp toàn diện các kỹ thuật gom nhóm hành động và loại bỏ tính đối ngẫu.

Thảo luận kết quả

Sự kết hợp giữa nhiều quản trị viên với các quyền hạn cục bộ dễ tạo ra các "đường dẫn tắt" ngoài tầm kiểm soát. Trong ví dụ thực nghiệm với 6 quy tắc ARBAC và 4 vị trí không gian, một nhân viên thực tập ban đầu chỉ có quyền đọc dữ liệu cơ bản đã được nâng cấp quyền ghi tập tin nhạy cảm tại tòa nhà A1 vào buổi chiều thông qua 2 bước gán quyền gián tiếp.

Dữ liệu thực nghiệm của nghiên cứu được trực quan hóa qua biểu đồ đường thể hiện thời gian thực thi theo số lượng vị trí địa lý (từ 1 đến 5 địa điểm) và biểu đồ cột so sánh thời gian xử lý trước và sau khi áp dụng các kỹ thuật Heuristic. Kết quả so sánh cho thấy phương pháp đề xuất vượt trội hơn các công cụ kiểm định truyền thống vốn bị nghẽn do bùng nổ không gian trạng thái (State Space Explosion) khi số lượng khung giờ tăng lên.

Đề xuất và khuyến nghị

Nhằm nâng cao an toàn thông tin khi áp dụng mô hình kiểm soát truy cập không - thời gian, các khuyến nghị cụ thể được đề xuất:

• Tích hợp công cụ kiểm định tự động vào quy trình CI/CD bảo mật: Đội ngũ kỹ sư an toàn hệ thống cần thiết lập việc kiểm tra tự động các tập chính sách phân quyền ASTRBAC trước khi đẩy lên môi trường thực tế, mục tiêu phát hiện sớm 100% lỗ hổng phân quyền trong vòng 2 tuần triển khai.
• Chuẩn hóa định dạng chính sách theo khung logic vị từ: Các kiến trúc sư giải pháp phần mềm cần chuẩn hóa toàn bộ tập luật phân quyền theo cấu trúc logic bậc nhất lớp BSR, hoàn thành chuyển đổi trong vòng 3 tháng nhằm đảm bảo khả năng tương thích với các công cụ kiểm chứng tự động.
• Áp dụng triệt để nguyên tắc phân tách trách nhiệm quản trị: Các tổ chức doanh nghiệp cần giới hạn phạm vi hiệu lực của mỗi quản trị viên theo đúng miền không gian và thời gian cụ thể, giảm thiểu 40% nguy cơ lạm dụng quyền hạn chéo giữa các phòng ban.
• Rà soát định kỳ tập luật phân quyền với các kỹ thuật Heuristic: Bộ phận an ninh mạng nên thực hiện quét định kỳ hàng tháng đối với toàn bộ các quy tắc can_assign và can_revoke, loại bỏ ít nhất 20% các quy tắc dư thừa nhằm tối ưu hóa hiệu năng hệ thống.

Đối tượng nên tham khảo luận văn

Luận văn mang lại giá trị học thuật và ứng dụng thực tiễn cao cho các nhóm đối tượng sau:

• Chuyên gia an toàn thông tin và Quản trị viên hệ thống: Nắm bắt cơ chế nhận diện rủi ro tiềm ẩn khi cấu hình chính sách phân quyền phân tán trên các hệ thống có hơn 500 người dùng.
• Kỹ sư thiết kế và Kiến trúc sư phần mềm: Ứng dụng mô hình ASTRBAC để thiết kế các kiến trúc kiểm soát truy cập phân tầng, linh hoạt theo ngữ cảnh vị trí GPS và lịch làm việc thực tế.
• Nghiên cứu sinh và Giảng viên ngành Khoa học Máy tính: Sử dụng phương pháp chuyển đổi logic BSR và bộ giải SMT làm tài liệu tham khảo cho các nghiên cứu về kiểm định mô hình hình thức.
• Doanh nghiệp vận hành hệ thống IoT và Smart Building: Ứng dụng các quy tắc ràng buộc không gian - thời gian để kiểm soát truy cập vật lý và logic cho hàng nghìn thiết bị đầu cuối.

Câu hỏi thường gặp

1. Bài toán User-Role Reachability trong ASTRBAC là gì? Đây là bài toán xác định xem liệu có tồn tại một chuỗi các thao tác quản trị hợp lệ khiến một người dùng bất kỳ đạt được một vai trò hoặc quyền hạn bị cấm tại một vị trí và thời điểm xác định hay không. Trong mô hình ASTRBAC, bài toán này trở nên phức tạp hơn do phải đồng thời thỏa mãn các ràng buộc về không gian và thời gian.

2. Công cụ ASASPSPACETIME hoạt động theo nguyên lý nào? Công cụ được lập trình bằng Python, đóng vai trò chuyển đổi các tập luật ASTRBAC thành các công thức logic vị từ bậc nhất thuộc lớp BSR. Sau đó, công cụ liên kết với bộ giải kiểm định mô hình biểu trưng MCMT để kiểm tra tính thỏa được của trạng thái vi phạm mục tiêu an toàn.

3. Tại sao cần áp dụng kỹ thuật Heuristic trong phân tích chính sách? Khi hệ thống có nhiều vai trò, khung giờ và địa điểm, không gian trạng thái kiểm định sẽ bùng nổ theo cấp số nhân. Các kỹ thuật Heuristic như Forwarding và Backwarding giúp loại bỏ hơn 50% các hành động không liên quan, giúp thuật toán kết thúc nhanh và tiết kiệm tài nguyên tính toán.

4. Mô hình ASTRBAC khác biệt gì so với ARBAC97 truyền thống? ARBAC97 chỉ quản lý việc gán và thu hồi vai trò tĩnh. ASTRBAC mở rộng bằng cách tích hợp ngữ cảnh không gian và thời gian vào cả điều kiện của quản trị viên lẫn điều kiện của người dùng, đồng thời hỗ trợ quản trị đa vai trò thay vì chỉ một vai trò đơn lẻ.

5. Luận văn có hỗ trợ phân tích khi số lượng người dùng là vô hạn không? Có. Nhờ việc chuyển đổi bài toán về dạng logic vị từ bậc nhất lớp BSR và giải quyết bằng kỹ thuật kiểm chứng mô hình biểu trưng modulo lý thuyết (MCMT), phương pháp đề xuất có thể kiểm định chính xác tính an toàn của hệ thống mà không cần biết trước số lượng người dùng cụ thể.

Kết luận

• Luận văn đã giải quyết trọn vẹn bài toán phân tích an toàn tự động cho mô hình kiểm soát truy cập ngữ cảnh không - thời gian ASTRBAC.
• Đóng góp phương pháp luận chuyển đổi hình thức từ chính sách bảo mật sang logic vị từ bậc nhất lớp BSR có thể quyết định được.
• Xây dựng thành công công cụ ASASPSPACETIME tích hợp bộ giải SMT MCMT với thời gian phản hồi thực nghiệm dưới 1.5 giây.
• Đề xuất 7 kỹ thuật Heuristic tối ưu giúp giảm thiểu đáng kể tình trạng bùng nổ không gian trạng thái trong quá trình kiểm định.
• Định hướng nghiên cứu tiếp theo trong giai đoạn 6 đến 12 tháng tới là mở rộng mô hình cho cấu trúc phân cấp vai trò (Role Hierarchy) phức tạp.

Các nhà phát triển hệ thống và chuyên gia bảo mật có thể ứng dụng ngay khung phân tích này để rà soát và củng cố hệ thống chính sách bảo mật của đơn vị mình.

Trích đoạn nội dung tài liệu

ĐẠ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.