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

ĐẠI HỌC QUỐC GIA HÀ NỘI

TRƯỜNG ĐẠI HỌC CÔNG NGHỆ

LƯƠNG THANH NHẠ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

LUẬN ÁN TIẾN SĨ CÔNG NGHỆ THÔNG TIN

Hà Nội - 2021

ĐẠI HỌC QUỐC GIA HÀ NỘI

TRƯỜNG ĐẠI HỌC CÔNG NGHỆ

LƯƠNG THANH NHẠ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

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.TS. Trương Ninh 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

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

5

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

Control

Access Điều khiển truy cập dựa trên thuộc

tính

API

Application Programming Giao diện lập trình ứng dụng

Interface

AST

CFG

DAC

Abstract Syntax Tree

Control Flow Graph

Cây cú pháp trừu tượng

Đồ thị luồng điều khiển

Discretionary Access Con- Điều khiển truy cập tùy ý

trol

FSA

Finite State Automata

Ôtômat hữu hạn trạng thái

HTML

Hypertext Markup Lan- Ngôn ngữ đánh dấu siêu văn bản

guage

IEC

ISO

International Electrotechni- Uỷ ban kỹ thuật điện quốc tế

cal Commission

International Organization Tổ chức tiêu chuẩn hoá quốc tế

for Standardization

MAC

MVC

NIST

Mandatory Access Control

Model-View-Controller

Điều khiển truy cập bắt buộc

Mô hình-Khung nhìn-Bộ điều khiển

National Institute of Stan- Viện Tiêu chuẩn và Kĩ thuật Quốc

dards and Technology

Push Down Automaton

Policy Decision Point

Policy Enforcement Point

gia Mỹ

PDA

PDP

PEP

PDG

PHP

Ôtômat đẩy xuống

Điểm quyết định chính sác

Điểm thực thi chính sách

Program Dependence Graph Đồ thị phụ thuộc chương trình

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

OASIS

Role-Based Access Control

Điều khiển truy cập dựa trên vai trò

Organization for the Ad- Tổ chức cải tiến các tiêu chuẩn

vancement of Structured In- thông tin có cấu trúc

formation Standards

viii

SDG

SoD

System Dependence Graph Đồ thị phụ thuộc hệ thống

Separation of Duties Phân chia nhiệm vụ

SpEL

SQL

Spring Expression Language Ngôn ngữ biểu thức Spring

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

URL

XACML

Unified Modeling Language Ngôn ngữ mô hình hóa thống nhất

Uniform Resource Locator Định vị tài nguyên thống nhất

eXtensible Access Control Ngôn ngữ đánh dấu kiểm soát truy

Markup Language cập mở rộng

XML

Extensible Markup Lan- Ngôn ngữ đánh dấu mở rộng

guage

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:2013¹, để 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

¹https://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ống đã được đặc tả nhất quán và đầy đủ với các yêu cầu của các

tổ chức. Các phương pháp chính được sử dụng trong quá trình thực hiện luận

án là phân tích mã nguồn, mô hình hóa và so sánh. Ngoài mục đích kiểm tra sự

phù hợp của chính sách truy cập được triển khai và đặc tả, các phương pháp đề

xuất của luận án còn cung cấp các thông tin về các quy tắc truy cập đã triển

khai không chính xác (nếu có) để giúp các nhà lập trình có thể lần vết và thực

hiện các điều chỉnh kịp thời.

Đối tượng nghiên cứu của luận án là chính sách điều khiển truy cập của hệ

thống web. Cụ thể là chính sách điều khiển truy cập theo vai trò và chính sách

điều khiển truy cập theo thuộc tính. Đồng thời, luận án quan tâm đến các mô

hình biểu diễn, đặc tả chính sách và các phương pháp triển khai chính sách trong

hệ thống ứng dụng. Từ đó, mã nguồn của ứng dụng được phân tích, tổng hợp

và kiểm chứng.

1.2. Nội dung nghiên cứu

Kiểm soát truy cập đã được chứng minh trong thực tiễn là một trong những

kỹ thuật hiệu quả để ngăn chặn các vi phạm truy cập nhằm đảm bảo các 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. Trong thực

tế, có nhiều mô hình kiểm soát truy cập đã được đề xuất [50, 83, 101] nhưng

điều khiển truy cập theo vai trò (RBAC) và điều khiển truy cập theo thuộc tính

(ABAC) là hai mô hình được triển khai phổ biến và hiệu quả trong các hệ thống

ứng dụng [44]. Tuy nhiên, việc đảm bảo tính chính xác của những chính sách

4

điều khiển truy cập này được triển khai trong các hệ thống ứng dụng ở giai đoạn

lập trình luôn là một thách thức lớn đối với các nhà phát triển phần mềm.

Bên cạnh đó, với nhiều thư viện được tích hợp để hỗ trợ cho việc triển khai

các chính sách điều khiển truy cập được an toàn, ngôn ngữ lập trình Java cũng

được các nhà lập trình thường lựa chọn để phát triển các sản phẩm của họ. Khi

đó, chính sách điều khiển truy cập của hệ thống có thể được triển khai theo

phương pháp an ninh lập trình và/hoặc an ninh khai báo theo kiến trúc MVC,

khung làm việc Spring Security. Vì thế, phạm vi nghiên cứu của luận án là các

hệ thống web được phát triển bởi JavaEE theo kiến trúc MVC, khung làm việc

Spring Security. Để hoàn thành các mục tiêu đã đề ra, luận án tập trung nghiên

cứu các nội dung chính sau:

Nghiên cứu các mô hình biểu diễn các chính sách điều khiển truy cập của

hệ thống phần mềm: đ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 (SecureUML), điều khiển truy cập theo

thuộc tính.

Nghiên cứu các phương pháp an ninh lập trình, an ninh khai báo để triển

khai chính sách RBAC, ABAC của các hệ thống web theo mô hình kiến

trúc MVC, khung làm việc Spring Security.

Đề xuất các phương pháp phân tích mã nguồn, biểu diễn chính sách điều

khiển truy cập của hệ thống web.

Đề xuất các thuật toán kiểm tra sự phù hợp của mô hình chính sách điều

khiển truy cập của hệ thống web và đặc tả.

Cài đặt các công cụ theo các phương pháp đã đề xuất để hỗ trợ quá trình

kiểm chứng tự động.

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

Sau quá trình giải quyết bài toán với mục tiêu, đối tượng và phương pháp

nghiên cứu đã đề ra, luận án có các đóng góp chính sau đây:

(i) Đề xuất 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. Các phương thức khai thác tài nguyên trong ứng

dụng web được trích rút thành danh sách quyền truy cập tài nguyên. Sau

đó kết hợp với thành phần Controller và V iew để xây dựng đồ thị khai

5