Luận án: 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 - TS Lương Thanh Nhạn
Luận án tiến sĩ công nghệ thông tin đề xuất 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, nâng cao hiệu quả và bảo mật.
Số trang
137
Thời gian đọc
21 phút
Lượt xem
0
Lượt tải
0
Phí lưu trữ
40 Point
Tổng quan nhanh
- Chủ đề:
- 1. Tầm quan trọng kiểm chứng chính sách điều khiển truy cập
- Số trang:
- 137 trang
- Trường:
- Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội
- Chuyên ngành:
- Kỹ thuật phần mềm
- Tác giả:
- Lương Thanh Nhạn
Tóm tắt nội dung luận án
I. Tầm quan trọng kiểm chứng chính sách điều khiển truy cập
Bảo mật hệ thống phần mềm đóng vai trò then chốt trong thời đại số. Các ứng dụng web hiện đại xử lý lượng dữ liệu khổng lồ. Lỗ hổng bảo mật gây tổn thất nghiêm trọng về tài chính và uy tín. Cơ chế điều khiển truy cập là tuyến phòng thủ đầu tiên. Cơ chế này kiểm soát quyền hạn của từng chủ thể đối với tài nguyên hệ thống. Tuy nhiên, quá trình hiện thực hóa quy tắc an ninh thường phát sinh sai sót. Lập trình viên dễ mắc lỗi cấu hình trong giai đoạn viết mã nguồn. Các lỗi bảo mật xuất hiện phổ biến trong kiến trúc Model-View-Controller (MVC). Việc phát hiện lỗi muộn làm tăng chi phí khắc phục. Kiểm chứng tự động từ mã nguồn giúp giảm thiểu rủi ro an ninh. Kỹ thuật phân tích tĩnh hỗ trợ rà soát toàn diện mã lệnh trước khi triển khai. Quá trình kiểm tra đảm bảo hệ thống tuân thủ chặt chẽ nguyên tắc đặc quyền tối thiểu (least privilege). Nhờ đó, chất lượng phần mềm được nâng cao và bảo vệ tài sản số an toàn.
1.1. Thách thức trong thực thi an ninh ứng dụng web
Ứng dụng web ngày nay đối mặt với nhiều cuộc tấn công leo thang đặc quyền. Lỗ hổng thường bắt nguồn từ sự bất đồng bộ giữa thiết kế và mã nguồn thực tế. Lập trình an ninh bao gồm an ninh lập trình (programmatic security) và an ninh khai báo (declarative security). Việc kết hợp hai hình thức này dễ tạo ra kẽ hở logic. Nhiều phương thức xử lý tài nguyên không được phân quyền chính xác. Người dùng trái phép có thể lợi dụng sơ hở để chiếm quyền điều khiển. Phương pháp kiểm thử truyền thống khó bao quát hết mọi nhánh rẽ thực thi. Việc đánh giá thủ công tốn nhiều thời gian và dễ bỏ sót lỗi nghiêm trọng. Vì vậy, giải pháp tự động hóa quá trình xác minh quy tắc an ninh là yêu cầu cấp thiết. Kỹ thuật phân tích tĩnh mã nguồn giúp phát hiện sớm các điểm yếu bảo mật. Cách tiếp cận này giúp tối ưu hóa chi phí vận hành và bảo trì hệ thống.
1.2. Áp dụng nguyên tắc đặc quyền tối thiểu trong mã nguồn
Nguyên tắc đặc quyền tối thiểu (least privilege) yêu cầu cấp quyền vừa đủ cho mỗi tác vụ. Mỗi vai trò người dùng chỉ được thao tác trên tài nguyên cần thiết. Việc cấp phát thừa quyền tạo điều kiện cho các cuộc tấn công khai thác lỗ hổng. Khi bị xâm nhập, tài khoản dư thừa đặc quyền sẽ gây hậu quả lan rộng. Do đó, việc rà soát sự tương thích giữa quyền thực tế và quyền đặc tả là bắt buộc. Hệ thống cần tự động phân tích đồ thị luồng điều khiển và luồng dữ liệu. Kỹ thuật phân tích tĩnh hỗ trợ trích xuất chính xác danh sách quyền từ mã nguồn Java. Quá trình đối sánh giúp loại bỏ các quyền truy cập dư thừa. Việc duy trì nguyên tắc đặc quyền tối thiểu giúp cô lập rủi ro và tăng cường độ vững chắc cho toàn bộ kiến trúc phần mềm.
II. Kiểm chứng chính sách điều khiển truy cập theo vai trò
Mô hình điều khiển truy cập dựa trên vai trò (RBAC) được sử dụng rộng rãi trong các hệ thống doanh nghiệp. RBAC phân bổ quyền hạn cho người dùng thông qua các vai trò trung gian. Tuy nhiên, việc hiện thực hóa RBAC bằng an ninh lập trình tiềm ẩn nhiều nguy cơ sai lệch. Quá trình kiểm chứng đòi hỏi trích xuất chính xác cấu trúc phân quyền từ mã nguồn. Các phương thức khai thác tài nguyên được định vị thông qua kỹ thuật phân tích cú pháp trừu tượng (AST). Hệ thống xây dựng đồ thị khai thác tài nguyên và danh sách các quyền tương ứng. Từ đó, một ma trận kiểm soát truy cập theo vai trò được thiết lập tự động. Ma trận này phản ánh trung thực hành vi phân quyền thực tế trong mã lệnh. Thuật toán kiểm tra sự phù hợp so sánh ma trận thực tế với chính sách đặc tả ban đầu. Quá trình này giúp phát hiện chính xác các sai lệch phân quyền trước khi hệ thống đi vào vận hành.
2.1. Trích xuất chính sách từ mã nguồn ứng dụng Java
Việc trích xuất cấu trúc phân quyền từ mã nguồn Java đòi hỏi phân tích cấu trúc cây cú pháp trừu tượng (AST). Quá trình phân tích tập trung vào các controller và service trong kiến trúc MVC. Các lệnh kiểm tra quyền nội hàm (programmatic checks) được nhận diện tự động. Thuật toán tiến hành phân tích các phương thức truy xuất tài nguyên nhạy cảm. Đồ thị khai thác tài nguyên (Resource Access Graph) được xây dựng từ các luồng thực thi. Đồ thị biểu diễn mối quan hệ giữa vai trò, hành động và tài nguyên mục tiêu. Danh sách quyền được tổng hợp thành ma trận kiểm soát truy cập theo vai trò. Ma trận cung cấp cái nhìn trực quan và toàn diện về hiện trạng bảo mật. Công cụ tự động hóa CheckingRBAC hỗ trợ thực thi quy trình này một cách nhanh chóng và chính xác. Nhờ đó, các lập trình viên có thể rà soát lỗi bảo mật ngay trong quá trình phát triển phần mềm.
2.2. Đánh giá sự phù hợp bằng công cụ CheckingRBAC
Công cụ CheckingRBAC được phát triển nhằm tự động hóa quy trình đối soát chính sách. Công cụ nhận đầu vào là mã nguồn dự án và tệp đặc tả chính sách chuẩn. CheckingRBAC thực hiện phân tích tĩnh để tạo ma trận kiểm soát truy cập theo vai trò. Sau đó, thuật toán so sánh hai mô hình để tìm ra điểm bất đồng bộ. Các trường hợp cấp quyền thiếu hoặc cấp quyền thừa đều được cảnh báo chi tiết. Báo cáo trực quan chỉ rõ vị trí dòng mã nguồn chứa lỗi logic an ninh. Việc tích hợp CheckingRBAC vào quy trình kiểm thử tự động giúp tiết kiệm đáng kể nguồn lực. Phương pháp kiểm chứng này nâng cao độ tin cậy của ứng dụng web doanh nghiệp. Kết quả thực nghiệm chứng minh công cụ phát hiện chính xác các lỗ hổng phân quyền phổ biến.
III. Kiểm chứng chính sách điều khiển truy cập ABAC hiệu quả
Mô hình điều khiển truy cập dựa trên thuộc tính (ABAC) cung cấp khả năng phân quyền linh hoạt và chi tiết. Quyết định truy cập dựa trên các thuộc tính của chủ thể, đối tượng, hành động và ngữ cảnh môi trường. Sự linh hoạt này đi kèm với độ phức tạp cao trong cấu hình và quản lý. Các quy tắc an ninh ABAC thường được biểu diễn bằng ngôn ngữ đặc tả chính sách XACML. Khi số lượng quy tắc tăng lên, nguy cơ xung đột và bất thường bảo mật xuất hiện thường xuyên. Việc kiểm chứng thủ công chính sách XACML gần như bất khả thi trong môi trường thực tế. Do đó, phương pháp tiếp cận tự động là giải pháp bắt buộc. Kỹ thuật phân tích tĩnh mã nguồn kết hợp chuyển đổi mô hình giúp đánh giá toàn diện chính sách ABAC. Hệ thống bảo đảm mọi yêu cầu truy cập đều được xử lý đúng theo thiết kế an ninh định trước.
3.1. Chuẩn hóa quy tắc với ngôn ngữ đặc tả chính sách XACML
Ngôn ngữ đặc tả chính sách XACML là tiêu chuẩn công nghiệp cho mô hình ABAC. XACML sử dụng cấu trúc XML để biểu diễn các tập quy tắc (PolicySet), chính sách (Policy) và quy tắc (Rule). Mỗi quy tắc bao gồm điều kiện (Condition), mục tiêu (Target) và hiệu lực (Effect) cho phép hoặc từ chối. Thuật toán kết hợp quy tắc (Rule Combining Algorithm) xác định kết quả cuối cùng khi có nhiều quy tắc cùng áp dụng. Tuy nhiên, tính phức tạp của cú pháp XACML dễ dẫn đến lỗi diễn giải sai. Việc đặc tả chính xác các điều kiện ngữ cảnh là yếu tố sống còn đối với an ninh hệ thống. Quá trình kiểm chứng bắt đầu từ việc chuẩn hóa và phân tích cú pháp tệp tin XACML. Cấu trúc cây quyết định được xây dựng để đơn giản hóa quá trình xử lý logic tiếp theo.
3.2. Chuyển đổi chính sách ABAC sang mô hình logic vị từ
Để phục vụ kiểm chứng tự động, các quy tắc XACML cần được chuyển đổi sang dạng biểu diễn toán học. Kỹ thuật mô hình hóa chuyển đổi từng phần tử XACML thành các công thức logic bậc nhất hoặc logic vị từ. Các thuộc tính chủ thể, đối tượng và môi trường trở thành các biến logic. Điều kiện cấp quyền được ánh xạ thành các mệnh đề logic ràng buộc. Phép chuyển đổi này giữ nguyên ngữ nghĩa bảo mật gốc của hệ thống. Biểu diễn logic cho phép áp dụng các thuật toán đại số Boole để đơn giản hóa biểu thức. Đây là bước chuẩn bị quan trọng để đưa bài toán kiểm chứng vào các bộ giải tự động. Việc chuẩn hóa hình thức giúp loại bỏ tính nhập nhằng của ngôn ngữ tự nhiên hoặc cấu trúc XML cồng kềnh.
IV. Phân tích xung đột chính sách và phát hiện bất thường
Trong các hệ thống phân quyền phức tạp, việc tích hợp nhiều quy tắc dễ dẫn đến sai sót logic. Phân tích xung đột chính sách (policy conflict analysis) là nhiệm vụ quan trọng nhằm đảm bảo an toàn vận hành. Xung đột xảy ra khi hai quy tắc đồng thời áp dụng cho một yêu cầu nhưng đưa ra quyết định trái ngược nhau. Bên cạnh đó, phát hiện bất thường chính sách (policy anomaly detection) giúp tìm ra các quy tắc bị dư thừa, che khuất hoặc không thể tiếp cận. Quy tắc bị che khuất (shadowed rule) khiến một số chính sách an ninh quan trọng không bao giờ được kích hoạt. Quy tắc dư thừa (redundant rule) làm chậm hiệu năng xử lý của bộ điều khiển truy cập. Việc phát hiện bất thường giúp tối ưu hóa bộ quy tắc và ngăn chặn các lỗ hổng truy cập trái phép. Kỹ thuật phân tích tĩnh kết hợp ma trận quyết định hỗ trợ nhận diện chính xác các bất thường này.
4.1. Kỹ thuật phân loại và nhận diện bất thường an ninh
Các bất thường trong chính sách truy cập được phân loại thành nhiều dạng cụ thể. Bất thường che khuất xuất hiện khi một quy tắc có phạm vi hẹp hơn đứng sau quy tắc tổng quát có hiệu lực trái ngược. Bất thường tương đương xảy ra khi hai quy tắc xử lý cùng tập thuộc tính và đưa ra cùng kết luận. Bất thường xung đột nảy sinh khi không có thuật toán kết hợp rõ ràng cho các quyết định đối lập. Bất thường bất khả thi (unreachable rule) chứa các điều kiện logic không bao giờ thỏa mãn. Kỹ thuật phân tích so sánh không gian thuộc tính giúp định vị từng loại bất thường. Quá trình kiểm tra quét qua toàn bộ tập chính sách để chỉ ra các điểm giao thoa có vấn đề. Kết quả phân loại hỗ trợ quản trị viên tái cấu trúc tập luật một cách khoa học và chính xác.
4.2. Tối ưu hóa và nâng cao tính nhất quán của chính sách
Đảm bảo tính nhất quán của chính sách (policy consistency) là mục tiêu cốt lõi của quản trị an toàn thông tin. Tính nhất quán khẳng định rằng không tồn tại bất kỳ mâu thuẫn logic nào trong không gian quyết định. Sau khi phát hiện bất thường, quy trình tối ưu hóa chính sách được tiến hành. Các quy tắc dư thừa bị loại bỏ để tăng tốc độ phản hồi của hệ thống. Thứ tự ưu tiên của các quy tắc được sắp xếp lại hợp lý nhằm triệt tiêu hiện tượng che khuất. Quản trị viên tiến hành gộp các quy tắc tương đương để tinh giản kích thước bộ cấu hình. Một bộ quy tắc nhất quán và tinh gọn giúp giảm thiểu sai sót khi mở rộng hệ thống trong tương lai. Nhờ đó, kiến trúc bảo mật duy trì sự ổn định và kiểm soát chặt chẽ mọi luồng dữ liệu.
V. Kiểm chứng hình thức và bộ giải SMT cho tính nhất quán
Kiểm chứng hình thức (formal verification) là phương pháp toán học nghiêm ngặt nhất để chứng minh tính đúng đắn của phần mềm. Trong an ninh truy cập, phương pháp này bảo đảm chính sách thỏa mãn các thuộc tính an toàn tuyệt đối. Kiểm tra mô hình (model checking) và giải thuật thỏa mãn mệnh đề được áp dụng mạnh mẽ. Bộ giải SMT (SMT solver - Z3) đóng vai trò là công cụ tính toán chủ lực trong quy trình kiểm chứng. SMT solver kiểm tra tính thỏa mãn của các công thức logic phức tạp đại diện cho không gian chính sách. Khi phát hiện vi phạm hoặc xung đột, bộ giải tự động sinh ra phản ví dụ (counterexample). Phản ví dụ cung cấp trường hợp cụ thể dẫn đến lỗi an ninh trong mã nguồn hoặc cấu hình. Việc tích hợp bộ giải Z3 mang lại tốc độ xử lý vượt trội và khả năng mở rộng cho các hệ thống phần mềm quy mô lớn.
5.1. Ứng dụng kiểm tra mô hình trong kiểm chứng hình thức
Kiểm tra mô hình (model checking) tiến hành duyệt toàn bộ không gian trạng thái của hệ thống điều khiển truy cập. Mô hình trạng thái biểu diễn các bước chuyển quyền và hành vi tương tác của người dùng. Thuộc tính an ninh được biểu diễn dưới dạng công thức logic thời gian (LTL hoặc CTL). Công cụ kiểm tra mô hình tự động rà soát xem thuộc tính an ninh có được bảo toàn trên mọi nhánh thực thi hay không. Phương pháp này đặc biệt hiệu quả trong việc phát hiện các lỗ hổng liên quan đến chuỗi hành động phức tạp. Nếu tồn tại kịch bản vi phạm, công cụ sẽ trích xuất vết thực thi dẫn tới trạng thái không an toàn. Nhờ đó, các kỹ sư phần mềm có thể nhanh chóng tái hiện và khắc phục điểm yếu logic. Kiểm tra mô hình nâng cao độ tin cậy và sự chuẩn xác tuyệt đối cho hệ thống.
5.2. Giải quyết bài toán ràng buộc với bộ giải SMT solver Z3
Bộ giải SMT (SMT solver - Z3) của Microsoft Research là công cụ hàng đầu trong chứng minh định lý tự động. Z3 hỗ trợ xử lý nhiều lý thuyết nền tảng như số học nguyên, mảng và kiểu dữ liệu đại số. Trong bài toán kiểm chứng truy cập, các ràng buộc thuộc tính được mã hóa thành các mệnh đề logic SMT-LIB. Z3 tiến hành kiểm tra tính thỏa mãn của mệnh đề phủ định thuộc tính an toàn. Nếu biểu thức thỏa mãn (SAT), Z3 cung cấp mô hình gán giá trị biến chứng minh sự tồn tại của lỗi bảo mật. Ngược lại, nếu biểu thức không thỏa mãn (UNSAT), chính sách được chứng minh là an toàn tuyệt đối. Việc kết hợp Z3 vào quy trình phân tích tĩnh giúp tự động hóa toàn diện khâu xác minh. Giải pháp này mang lại hiệu năng cao và độ chính xác vượt trội cho các ứng dụng thực tế.
Mục lục chi tiết luận án
Tải xuống file đầy đủ để xem toàn bộ nội dung
Tải đầy đủ (137 trang)Trích đoạn nội dung luận án
Tải xuống để đọc toàn bộĐẠ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 LUẬN ÁN TIẾN SĨ CÔNG NGHỆ THÔNG TIN Hà Nội - 20 ĐẠ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 Chuyên ngành: Kỹ thuật phần mềm Mã số: 9480103.01 LUẬN ÁN TIẾN SĨ CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS. Trương Ninh Thuận Hà Nội - 20 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.
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. 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. 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.
Nội dung nghiên cứu. Đóng góp của luận án. Cấu trúc luận án. KIẾN THỨC CƠ SỞ.
An ninh phần mềm. 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ột số mô hình chính sách điều khiển truy cập.
Điều khiển truy cập theo vai trò. Ngôn ngữ mô hình hóa chính sách an ninh thống nhất. Điều khiển truy cập theo thuộc tính. Triển khai chính sách điều khiển truy cập trong JavaEE.
An ninh truy cập trong JavaEE. Một số kiến trúc thiết kế phần mềm trong JavaEE. Phân tích và biểu diễn chương trình. Phân tích chương trình.
Một số phương pháp biểu diễn chương trình. Tóm tắt chương. KIỂM CHỨNG CHÍNH SÁCH RBAC TRIỂN KHAI THEO PHƯƠNG PHÁP AN NINH LẬP TRÌNH. Các nghiên cứu liên quan.
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. Tập quy tắc truy cập đặc tả. Danh sách các quyền. Đồ thị khai thác tài nguyên.
Ma trận kiểm soát truy cập theo vai trò. 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ả. Công cụ kiểm chứng. Giao diện công cụ.
Thảo luận và đánh giá. Tóm tắt chương. 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. Các nghiên cứu liên quan.
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. Kiểm tra phép gán người dùng - vai trò. Kiểm tra phép gán vai trò - quyền. Công cụ kiểm chứng.
Kiến trúc của công cụ. Giao diện đồ họa của công cụ. Thảo luận và đánh giá. 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. Các nghiên cứu liên quan. 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ính sách ABAC đặc tả của hệ thống. Chính sách ABAC triển khai trong ứng dụng. Các thuật toán kiểm chứng chính sách ABAC. Công cụ kiểm chứng.
Xây dựng công cụ. Thảo luận và đánh giá. Tóm tắt chương. 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 .
Nội dung được bảo vệ bản quyền — Tải xuống đầy đủ
Trích dẫn luận án này
Lương Thanh Nhạn (n.d.). Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm [Luận án tiến sĩ, Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội]. LuanAn.net. https://luanan.net/cong-nghe-thong-tin/an-toan-thong-tin/kiem-chung-chinh-sach-dieu-khien-truy-cap-phan-mem
Câu hỏi thường gặp
Luận án "Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm" nghiên cứu về vấn đề gì?
Luận án tiến sĩ công nghệ thông tin đề xuất 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, nâng cao hiệu quả và bảo mật.
Luận án "Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm" được bảo vệ tại trường nào?
Luận án này được bảo vệ tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội.
Luận án "Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm" thuộc chuyên ngành gì?
Luận án "Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm" thuộc chuyên ngành Kỹ thuật phần mềm. Danh mục: An Toàn Thông Tin.
Luận án "Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm" có bao nhiêu trang?
Luận án "Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm" có 137 trang. Bạn có thể xem trước một phần tài liệu ngay trên trang web trước khi tải về.
Cách tải luận án "Kiểm chứng chính sách điều khiển truy cập hệ thống phần mềm" về máy như thế nào?
Để tải luận án về máy, bạn nhấn nút "Tải xuống ngay" trên trang này, sau đó hoàn tất thanh toán phí lưu trữ. File sẽ được tải xuống ngay sau khi thanh toán thành công. Hỗ trợ qua Zalo: 0559 297 239.