ĐẠI HỌC MỘT SỐ PHƯƠNG PHÁP KIỂM CHỨNG CÁC CHÍNH SÁCH ĐIỀU KHIỂN TRUY CẬP CHO HỆ THỐNG PHẦN MỀM

Tìm hiểu các phương pháp kiểm chứng chính sách điều khiển truy cập cho hệ thống phần mềm, đảm bảo an ninh và chất lượng ứng dụng web Java theo kiến trúc MVC.

Chuyên ngành

Kỹ thuật phần mềm

Người đăng

Ẩn danh

Thể loại

Luận án Tiến sĩ

20

137
3
0

Phí lưu trữ

35 Point

Mục lục chi tiết

LỜI CAM ĐOAN

LỜI CẢM ƠN

TÓM TẮT

1. CHƯƠNG 1: NỘI DUNG NGHIÊN CỨU

1.1. Đóng góp của luận án

1.2. Cấu trúc luận án

1.3. KIẾN THỨC CƠ SỞ

1.3.1. An ninh phần mềm

1.3.2. Một số tính chất an ninh của phần mềm

1.3.3. Chính sách điều khiển truy cập

1.3.4. Một số mô hình chính sách điều khiển truy cập

1.3.5. Điều khiển truy cập theo vai trò

1.3.6. Ngôn ngữ mô hình hóa chính sách an ninh thống nhất

1.3.7. Điều khiển truy cập theo thuộc tính

1.3.8. Triển khai chính sách điều khiển truy cập trong JavaEE

1.3.9. An ninh truy cập trong JavaEE

1.3.10. Một số kiến trúc thiết kế phần mềm trong JavaEE

1.3.11. Phân tích và biểu diễn chương trình

1.3.11.1. Phân tích chương trình
1.3.11.2. Một số phương pháp biểu diễn chương trình

1.3.12. Tóm tắt chương

2. KIỂM CHỨNG CHÍNH SÁCH RBAC TRIỂN KHAI THEO PHƯƠNG PHÁP AN NINH LẬP TRÌNH

2.1. Các nghiên cứu liên quan

2.2. 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

2.2.1. Tập quy tắc truy cập đặc tả

2.2.2. Danh sách các quyền

2.2.3. Đồ thị khai thác tài nguyên

2.2.4. Ma trận kiểm soát truy cập theo vai trò

2.2.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ả

2.2.6. Công cụ kiểm chứng

2.2.6.1. Giao diện công cụ

2.2.7. Thảo luận và đánh giá

2.2.8. Tóm tắt chương

3. 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

3.1. Các nghiên cứu liên quan

3.2. 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

3.2.1. Kiểm tra phép gán người dùng - vai trò

3.2.2. Kiểm tra phép gán vai trò - quyền

3.2.3. Công cụ kiểm chứng

3.2.3.1. Kiến trúc của công cụ
3.2.3.2. Giao diện đồ họa của công cụ

3.2.4. Thảo luận và đánh giá

3.2.5. Tóm tắt chương

4. KIỂM CHỨNG CHÍNH SÁCH ĐIỀU KHIỂN TRUY CẬP THEO THUỘC TÍNH

4.1. Các nghiên cứu liên quan

4.2. Phương pháp kiểm chứng chính sách điều khiển truy cập theo thuộc tính

4.2.1. Chính sách ABAC đặc tả của hệ thống

4.2.2. Chính sách ABAC triển khai trong ứng dụng

4.2.3. Các thuật toán kiểm chứng chính sách ABAC

4.2.4. Công cụ kiểm chứng

4.2.4.1. Xây dựng công cụ

4.2.5. Thảo luận và đánh giá

4.2.6. Tóm tắt chương

4.3. Hướng phát triển

DANH MỤC CÁC CÔNG TRÌNH KHOA HỌC

TÀI LIỆU THAM KHẢO

Tóm tắt

I. Tổng Quan Vì Sao Cần Kiểm Chứng Chính Sách Truy Cập

Các hệ thống phần mềm ngày càng được sử dụng rộng rãi, tiềm ẩn nhiều nguy cơ bảo mật. Điều khiển truy cập là một biện pháp hiệu quả để thực thi chính sách an ninh, 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 thường tiềm ẩn lỗi, đặc biệt trong giai đoạn lập trình. Việc phát hiện lỗi muộn sẽ tốn kém chi phí sửa chữa và gây ra hậu quả nghiêm trọng. Vì vậy, kiểm chứng từ mã nguồn ứng dụng là rất quan trọng để đảm bảo chính sách điều khiển truy cập được triển khai chính xác, mang lại hiệu quả kinh tế và nâng cao chất lượng phần mềm. Luận án này tập trung vào việc đề xuất các phương pháp kiểm chứng chính sách điều khiển truy cập cho các hệ thống web dựa trên kỹ thuật phân tích tĩnh, giúp phát hiện sớm các lỗ hổng bảo mật.

1.1. An Ninh Phần Mềm Nguy Cơ Tiềm Ẩn Trong Hệ Thống Web

Hệ thống web hiện nay đối mặt với nhiều nguy cơ bảo mật và khai thác tài nguyên trái phép. Các biện pháp bảo vệ chia thành 3 nhóm: xây dựng ứng dụng an toàn, áp dụng biện pháp bảo vệ (proxy), và thiết lập thành phần cơ sở hạ tầng để giám sát. Để bảo vệ tài nguyên, chính sách an ninh là cần thiết, bao gồm mã hóa, điều khiển truy cập và truyền thông an toàn.

1.2. Điều Khiển Truy Cập Biện Pháp Đảm Bảo An Toàn và Bảo Mật

Điều khiển truy cập là biện pháp quan trọng để đảm bảo tính bảo mật, toàn vẹn và sẵn sàng của hệ thống phần mềm. Tuy nhiên, việc triển khai chính sách điều khiển truy cập luôn tiềm ẩn lỗ hổng an ninh, do không tuân thủ hoặc bỏ sót yêu cầu an ninh. Lỗi lập trình, hiểu sai yêu cầu đặc tả cũng là nguyên nhân. Phần mềm càng lớn, việc triển khai càng phức tạp và dễ sai sót.

II. Thách Thức và Hướng Tiếp Cận trong Kiểm Chứng Truy Cập

Bài toán kiểm chứng chính sách điều khiển truy cập là một nhiệm vụ quan trọng giúp phát hiện sớm sai sót và đảm bảo tính an ninh phần mềm. Các nghiên cứu hiện tại tiếp cận theo nhiều hướng, từ xây dựng mô hình, đặc tả tính chất an ninh, đến phân tích và thẩm định chính sách điều khiển truy cập ở nhiều giai đoạn phát triển. Một số phương pháp còn xây dựng công cụ để tự động phát hiện lỗ hổng bảo mật từ mã nguồn. Luận án này tập trung vào các hệ thống web xây dựng bằng Java, theo kiến trúc MVC và áp dụng chính sách điều khiển truy cập theo vai trò hoặc thuộc tính.

2.1. Phân Tích Tĩnh Nền Tảng của Phương Pháp Kiểm Chứng

Luận án đề xuất các phương pháp kiểm chứng dựa trên nền tảng của kỹ thuật phân tích tĩnh. Phân tích tĩnh kiểm tra mã nguồn mà không cần thực thi, giúp xác định các lỗ hổng tiềm ẩn. Tuy nhiên, phương pháp này có thể đưa ra cảnh báo sai. Phân tích động, ngược lại, đảm bảo tính đúng đắn của lỗ hổng được xác định, nhưng không thể đảm bảo tính đầy đủ.

2.2. Kiểm Chứng RBAC và ABAC Hai Hướng Nghiên Cứu Chính

Luận án tập trung vào hai mô hình điều khiển truy cập: Kiểm soát truy cập dựa trên vai trò (RBAC)Kiểm soát truy cập dựa trên thuộc tính (ABAC). Các nghiên cứu về RBAC chủ yếu kiểm tra phép gán giữa quyền và vai trò. Với ABAC, một số nghiên cứu tập trung vào đặc tả, triển khai và kiểm thử chính sách điều khiển truy cập với Spring Security, nhưng chưa xác minh tính bảo mật chỉ bằng phân tích mã nguồn.

2.3. Mục tiêu chung của luận án bao gồm

(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...'

III. Kiểm Chứng Chính Sách RBAC An Ninh Lập Trình Giải Pháp

Luận án đề xuất phương pháp kiểm chứng chính sách điều khiển truy cập theo vai trò (RBAC) triển khai theo phương pháp an ninh lập trình. Chính sách RBAC của ứng dụng web được trích rút thông qua phân tích phương thức khai thác tài nguyên, xây dựng danh sách quyền và đồ thị khai thác tài nguyên. 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 quy tắc truy cập. Thuật toán kiểm tra sự phù hợp giữa ma trận kiểm soát và chính sách truy cập đã đặc tả được đề xuất. Công cụ CheckingRBAC được xây dựng để hỗ trợ.

3.1. Trích rút các quyền truy cập từ mã

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.

3.2. Xây dựng ma trận kiểm soát truy cập

Xây dựng ma trận kiểm soát truy cập tài nguyên theo vai trò. Ma trận này biểu diễn các quy tắc truy cập của hệ thống web. 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ả.

3.3. CheckingRBAC Tool

Xây dựng công cụ CheckingRBAC để hỗ trợ quá trình kiểm chứng theo phương pháp đã đề xuất.

IV. RBAC và Ràng Buộc Kiểm Chứng An Ninh Khai Báo Chi Tiết

Luận án đề xuất phương pháp kiểm chứng chính sách điều khiển truy cập 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. Chính sách điều khiển truy cập và ràng buộc cấp quyền được kiểm tra thông qua phép gán vai trò - người dùng và vai trò - quyền. Phép gán thứ nhất dựa trên phân tích cơ sở dữ liệu. Với phép gán thứ hai, quy tắc truy cập được phân tích và biểu diễn thành cây phân tích quy tắc truy cập. Thuật toán kiểm tra tính chính xác của phép gán đã triển khai được đề xuất. Công cụ VeRA được xây dựng.

4.1. Kiểm tra phép gán user role

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

4.2.Kiểm tra phép gán role permission

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ò.

4.3. VeRA Tool

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.

V. Kiểm Chứng ABAC Giải Pháp Cho Hệ Thống An Toàn

Luận án đề 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 (ABAC). Tiến trình kiểm chứng thực hiện bằng cách trích rút và phân tích quy tắc truy cập trong hệ thống web. Sự phù hợp giữa chính sách điều khiển truy cập và đặc tả được tiến hành thông qua định nghĩa hình thức và thuật toán kiểm tra tính bảo mật, toàn vẹn và sẵn sàng. Công cụ kiểm chứng APVer đã được phát triển.

5.1. Phân tích quy tắc truy cập

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.

5.2. Xác minh và bảo đảm ABAC

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.

5.3. APVer Tool

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.

VI. Kết Luận và Hướng Phát Triển Kiểm Chứng Chính Sách

Luận án đã đề xuất các phương pháp kiểm chứng chính sách điều khiển truy cập hiệu quả cho hệ thống phần mềm. Các công cụ CheckingRBAC, VeRA và APVer đã được xây dựng và thử nghiệm thành công. Hướng phát triển tiếp theo có thể tập trung vào việc mở rộng phạm vi áp dụng cho các loại hình hệ thống phần mềm khác, cải thiện hiệu suất của thuật toán kiểm chứng, và tích hợp các công cụ vào quy trình phát triển phần mềm.

6.1. Mở Rộng Phạm Vi Ứng Dụng

Mở rộng phạm vi áp dụng cho các loại hình hệ thống phần mềm khác.

6.2. Cải Thiện Hiệu Suất

Cải thiện hiệu suất của thuật toán kiểm chứng.

6.3. Tích Hợp Quy Trình

Tích hợp các công cụ vào quy trình phát triển phần mềm.

15/05/2025
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

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

Mở đầu của chương là một số tính chất an ninh của phần mềm, chính sách điều khiển truy cập. Ở mục kế tiếp, luận án trình bày về một số mô hình phổ biến được sử dụng để biểu diễn chính sách điều khiển truy cập của các hệ thống phần mềm. Các phương pháp triển khai mã an ninh truy cập và một số kiến trúc thiết kế phần mềm trong JavaEE được mô tả trong Mục 2. Cuối cùng, Mục 2.4 giới thiệu một số phương pháp phân tích mã nguồn và biểu diễn chương trình phần mềm.

Chương 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, đầu tiên của chương này sẽ trình bày các bước phân tích mã nguồn để xây dựng danh sách các quyền, đồ thị khai thác tài nguyên và ma trận kiểm soát truy cập theo vai trò của các ứng dụng web. Tiếp theo, hai thuật toán được đề xuất để xây dựng ma trận kiểm soát truy cập theo vai trò từ đồ thị khai thác tài nguyên và kiểm tra sự phù hợp của chính sách điều khiển truy cập trong ứng dụng web và đặc tả. Cuối cùng, một công cụ kiểm chứng tên 7 là CheckingRBAC được xây dựng theo phương pháp đề xuất và tiến hành thực nghiệm với hệ thống quản lý hồ sơ y tế. Chương 4 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 tập trung đề xuất các phương pháp phân tích cơ sở dữ liệu và mã nguồn của ứng dụng web để phục vụ cho quá trình kiểm chứng phép gán vai trò - người dùng và phép gán vai trò - quyền trong chính sách điều khiển truy cập của hệ thống.

Một cây phân tích các quy tắc truy cập theo vai trò được giới thiệu để biểu diễn chính sách cấp quyền theo vai trò trong ứng dụng web. Sau đó, hai thuật toán được đề xuất để phát hiện những phép gán không được triển khai chính xác như trong đặc tả. Công cụ VeRA được phát triển để hỗ trợ quá trình kiểm chứng tự động theo phương pháp đề xuất. Một số thực nghiệm của công cụ đã được tiến hành với chính sách điều khiển truy cập của hệ thống quản lý hồ sơ y tế.

Chương 5 Phương pháp kiểm chứng chính sách điều khiển truy cập theo thuộc tính, chương này đề xuất phương pháp phân tích và xây dựng tập quy tắc truy cập từ mã nguồn của ứng dụng web. Sự phù hợp của chính sách truy cập trong ứng dụng web với đặc tả của nó được thực hiện thông qua các định nghĩa hình thức và 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 hệ thống. Phương pháp đề xuất đã được triển khai thành công cụ kiểm chứng APVer và thực nghiệm với các kịch bản vi phạm tính bảo mật, tính toàn vẹn và tính sẵn sàng của hệ thống quản lý hồ sơ y tế. Cuối cùng là Chương 6 Kết luận.

Chương này tiến hành phân tích về các ưu, nhược điểm của từng phương pháp đã đề xuất và so sánh với một số phương pháp nghiên cứu liên quan. Từ đó, luận án thảo luận về các hướng nghiên cứu tiếp theo trong tương lai. 8 Chương 2 KIẾN THỨC CƠ SỞ Trong chương này, luận án sẽ trình bày về những kiến thức cơ sở được sử dụng trong các chương tiếp theo. Ở mục đầu tiên của chương, luận án trình bày về một số tính chất an ninh và chính sách điều khiển truy cập của các hệ thống phần mềm.

Tiếp theo, Mục 2.2 sẽ giới thiệu về một số mô hình biểu diễn chính sách điều khiển truy cập của các hệ thống phần mềm như điều khiển truy cập theo vai trò (RBAC), ngôn ngữ mô hình hóa chính sách an ninh thống nhất (SecureUML) và điều khiển truy cập theo thuộc tính (ABAC). Trong mục tiếp theo, luận án trình bày về phương pháp triển khai chính sách điều khiển truy cập trong JavaEE và một số kiến trúc được sử dụng trong quá trình thiết kế các hệ thống web. Cuối cùng, Mục 2.4 nêu một số phương pháp, công cụ hiện có được sử dụng trong phân tích chương trình và một số phương pháp biểu diễn chương trình. An ninh phần mềm Phần mềm đang được sử dụng rộng rãi trong nhiều lĩnh vực của đời sống xã hội, văn hóa, v.

Do đó, chất lượng của phần mềm có ảnh hưởng trực tiếp hoặc/và gián tiếp đến người sử dụng. Bên cạnh những lợi ích mà phần mềm mang lại, thì cũng xuất hiện nhiều vấn đề vi phạm truy cập tài nguyên làm ảnh hưởng đến chất lượng phần mềm và người dùng trong hệ thống [39, 60, 91, 99, 100, 102]. Một số sự cố an ninh phổ biến hay được nhắc đến là thất thoát hoặc làm sai lệch các thông tin riêng tư, quan trọng do hệ thống quản lý. Trong nghiên cứu [39], năm 2013, tập đoàn Target Corporation của Mỹ đã phát hiện ra thông tin thẻ ghi nợ và thẻ tín dụng cũng như thông tin địa chỉ, thư điện tử và số điện thoại của khoảng 70 triệu khách hàng đã bị xâm phạm.

Chi phí khắc phục vụ vi phạm này ước tính là 300 triệu đô la. Hay vi phạm dữ liệu của công ty Sony Pictures Entertainment đã ảnh hưởng đến hơn 3.000 máy tính khi bị phá hủy dữ liệu và phần mềm khởi động. Việc tin tặc xâm phạm mạng PlayStation của Sony vào năm 2011 đã ảnh hưởng đến khoảng 100 triệu tài khoản khách hàng và công ty phải đối mặt với chi phí khắc phục ít nhất là 9 171 triệu đô la. Thêm vào đó là vụ gian lận của Sony dẫn đến việc những bộ phim chưa được phát hành đã bị chia sẻ.

Cũng trong nghiên cứu này, với một số loại hình tổ chức cơ bản thì năm 2015 chứng kiến 24% vi phạm trong các công ty công nghệ, 19% trong các tổ chức y tế và 14% trong giải trí. Tương tự, năm 2016, những vi phạm từ các tổ chức được báo cáo là công nghệ (21%), y tế (17%), xã hội (8%) và chính phủ (8%). Theo Viện Tiêu chuẩn và Công nghệ Quốc gia của Mỹ (National Institute of Standards and Technology - NIST) năm 2012, các cuộc tấn công an ninh mạng đang gia tăng về số lượng, tính đa dạng, mức độ thiệt hại. Trong nghiên cứu của viện Ponemon1 năm 2017 với 419 công ty trong 13 quốc gia thì trung bình chi phí cho một vi phạm dữ liệu là 3,62 triệu đô la; 141 đô là là chi phí trung bình cho mỗi bản ghi bị mất hoặc bị đánh cắp; khả năng tái xảy ra vi phạm an ninh trong hai năm tiếp theo là 27,7%.

Theo báo cáo về các mối đe dọa an ninh Internet năm 2019 của Symantec2 , các kiểu tấn công và vi phạm an ninh ngày càng tinh vi. Một số loại phổ biến là Formjacking (một loại mã độc cài vào trang web để lấy cắp thông tin của khách hàng) hay Ransomware (ngăn chặn người dùng truy cập và sử dụng tài nguyên của họ). Trong đó, chiếm đến 56% là các vụ tấn công web. Bên cạnh đó, các nghiên cứu [60, 91] cũng cho thấy số các vi phạm dữ liệu cá nhân trong lĩnh vực như y tế thống kê được là tăng thường xuyên.

Thực tế cho thấy, an ninh phần mềm đã trở thành một tiêu chí quan trọng trong việc đánh giá các hệ thống phần mềm trong giai đoạn hiện nay. Để hạn chế các vi phạm an ninh, các nhà phát triển thường phải xây dựng, triển khai và đảm bảo chính sách an ninh trong các sản phẩm phần mềm của họ nhằm đáp ứng các yêu cầu an ninh của khách hàng. Khi đó, sự phù hợp của chính sách an ninh được triển khai trong mỗi hệ thống ứng dụng với các yêu cầu của nó sẽ được thể hiện thông qua các tính chất an ninh của phần mềm. Một số tính chất an ninh của phần mềm Các tính chất an ninh của phần mềm đã được nhiều tổ chức, nhà nghiên cứu xem xét ở nhiều khía cạnh theo từng quan điểm và thời điểm nghiên cứu khác nhau.

Tuy nhiên, các tính chất an ninh phổ biến nhất được nhắc đến là bộ ba C-I-A (Confidentiality - Integrity - Availability) [20, 74]. Ba tính chất này xuất hiện sớm nhất năm 1972 trong tài liệu của James P.Anderson’s và được thảo 1 https://www.org/library/2017-cost-of-data-breach-study-united-states 2 https://www.com/security-center/threat-report 10 luận nhiều trong các nghiên cứu sau đó. Trong đó: tính bảo mật (confidentiality) đảm bảo thông tin chỉ có thể truy cập bởi người dùng có quyền; tính toàn vẹn (integrity) bảo vệ tính chính xác và đầy đủ của thông tin và chỉ được sửa đổi bởi người có thẩm quyền; tính sẵn sàng (availability) đảm bảo rằng người dùng hợp pháp được truy cập thông tin và các tài sản liên quan khi cần. Sau đó, ISO 7498-2 đã bổ sung thêm hai tính chất để phù hợp cho mạng truyền thông là tính xác thực (authentication - khả năng hệ thống xác nhận danh tính của người gửi) và tính chống chối bỏ/tính trách nhiệm (nonrepudiation/accountablility - người gửi không thể từ chối những gì họ đã thao tác trong hệ thống).

Tiếp theo đó, Bộ Quốc phòng Mỹ đã bổ sung tính có khả năng kiểm toán (auditability) để theo dõi tất cả các hành động liên quan đến tài nguyên. Bên cạnh đó, theo nghiên cứu của Mead và các đồng tác giả [65], một số các tính chất an ninh cốt lõi của phần mềm gồm tính bảo mật (confidentiality), tính toàn vẹn (integrity), tính sẵn sàng (availability), tính trách nhiệm (accountabil- ity) và tính chống chối bỏ (non-repudiation). Ngoài ra còn một số tính chất khác có ảnh hưởng gián tiếp đến vấn đề an ninh phần mềm. Tất cả các tính chất này được mô tả như trong Hình 2.1: Một số tính chất an ninh của phần mềm.

ˆ Tính bảo mật: phần mềm phải đảm bảo rằng, các tính năng của của phần mềm, tài sản do phần mềm quản lý và/hoặc nội dung của tài sản sẽ được che giấu hoặc ẩn bởi các thực thể trái phép nhưng phải sẵn sàng cho các thực thể hợp pháp. Điều này còn phải thích hợp cả với các trường hợp phần mềm nguồn mở. ˆ Tính toàn vẹn: Phần mềm và các tài sản mà nó quản lý phải có tính bền và phục hồi đối với các tấn công an ninh nhằm sửa đổi trái phép mã nguồn, 11 tài sản nó quản lý, cấu hình của các thực thể hợp pháp, hoặc bất cứ sửa đổi nào khác từ những thực thể bất hợp pháp. Những sửa đổi có thể gồm việc ghi đè, làm hỏng, giả mạo, phá hoại, chèn (gồm cả mã độc) hoặc xóa.

Tính toàn vẹn phải bảo toàn cả trong khi thực thi và phát triển phần mềm.

Nội dung được bảo vệ bản quyền — Tải xuống đầy đủ

Trong bối cảnh an toàn thông tin ngày càng được chú trọng, việc 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 trở thành yêu cầu thiết yếu để đảm bảo tính bảo mật và toàn vẹn dữ liệu. Tài liệu này trình bày một số phương pháp kiểm chứng hiệu quả, từ phân tích mô hình hình thức đến kiểm thử tự động, giúp phát hiện và ngăn chặn lỗ hổng trong cơ chế phân quyền. Người đọc sẽ nắm được quy trình đánh giá tính đúng đắn của các mô hình RBAC, ABAC và nhiều cơ chế kiểm soát truy cập phổ biến hiện nay. Để mở rộng hiểu biết về lĩnh vực liên quan, bạn có thể tham khảo thêm kiểm chứng tự động hệ thời gian thực — một hướng nghiên cứu bổ trợ quan trọng trong xác minh hành vi hệ thống phần mềm phức tạp.