Đề tài Kiểm chứng cơ chế bảo mật dựa trên ast

i ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ---------- Nguyễn Văn Thanh KIỂM CHỨNG CƠ CHẾ BẢO MẬT DỰA TRÊN AST KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin HÀ NỘI – 2009 ii ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ ---------- Nguyễn Văn Thanh KIỂM CHỨNG CƠ CHẾ BẢO MẬT DỰA TRÊN AST KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ thông tin Cán bộ hướng dẫn: TS. Trương Ninh Thuận HÀ NỘI – 2009 iii Lời cảm ơn Em xin gửi lời cảm ơn chân thành nhất đến TS. Trương Ninh Thuận, người thầy đã cho em định hướng, những ý kiến quý báu về kiểm chứng cơ chế bảo mật dựa trên AST và đã tận tình hướng dẫn em hoàn thành khóa luận. Thầy đã giúp đỡ em rất nhiều và đi cùng em trong suốt thời gian thực hiện khóa luận. Thầy chỉ cho em cách tiếp cận, nghiên cứu một công nghệ mới, cách tìm ra giải pháp cho vấn đề mắc phải. Em xin chân thành cảm ơn quý thầy cô và các bạn đã giúp đỡ em trong những năm học qua. Em xin chân thành cảm ơn 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ạo điều kiện thuận lợi cho em trong suốt quá trình học tập và làm khóa luận này. Đề tài “Kiểm chứng cơ chế bảo mật dựa trên AST” là một đề tài khá mới mẻ lại được hoàn thành trong quỹ thời gian hạn hẹp nên khó tránh khỏi những khiếm khuyết em mong nhận được những góp ý chân thành từ thầy cô giáo và các bạn để đề tài có thể được mở rộng và nghiên cứu kỹ hơn, đưa vào trong thực tiễn ngành Công nghệ thông tin hiện nay. Hà Nội, ngày 10 tháng 5 năm 2009 Sinh viên Nguyễn Văn Thanh iv Danh sách các hình vẽ Hình 2.1: Một họ của các mô hình RBAC Hình 2.2: Mô hình RBAC0 Hình 2.3: Các ví dụ của Role Hierarchies Hình 2.4: Role Hierarchies cho một dự án Hình 2.5: Mô hình tổng quát của RH (RBAC1) Hình 2.6: Mô hình RBAC quản lý Hình 3.1: Cấu trúc tổng quát CDT Hình 3.2: Cấu trúc chi tiết của CDT Hình 3.3: Giao diện DOM AST Hình 3.4: Mô tả cách duyệt cây Hình 4.1: Cấu trúc cây của ifStatement đơn giản Hình 4.2: Mô tả thuật toán kiểm chứng cơ chế bảo mật Hình 4.3: Cấu trúc của lệnh if phức tạp Hình 4.4: Thể hiện phức tạp trên AST Hình 4.4: Lỗi thể hiện trong đoạn mã Hình 5.1: Giao diện StartPage sau khi cài CDT Hình 5.2: Cấu trúc DOM AST Hình 5.3: Giao diện chương trình Test Hình 5.4: Giao diện khi chạy Test thành công Hình 5.5: Giao diện kết quả Hình 5.6, 5.7: Minh họa kết quả kiểm tra chương trình. v Danh sách các thuật ngữ và khái niệm THUẬT NGỮ KHÁI NIỆM MAC Mandatory access control – điều khiển truy cập bắt buộc DAC Discretionary access control – điều khiển truy cập tùy quyền RBAC Role-based access control – điều khiển truy cập trên cơ sở vai trò ACL Access control list – Danh sách điều khiển truy cập Role hierarchy Cấp bậc trong vai trò OPS Tập hợp các hành động trên một đối tượng cụ thể Test Quá trình chạy một chương trình để kiểm tra một thuật toán hay một bài toán cụ thể. File Đối tượng tệp văn bản được sao lưu trên máy tính Project Nói về một dự án được tạo ra cụ thể là Eclipse Session Phiên làm việc User Người sử dụng Permission Quyền hạn Role Vai trò Expression Các biểu thức (Ở đây tập trung nói về các biểu thức điều kiện) vi Tóm tắt khóa luận Từ trước đến nay, bảo mật thông tin luôn chiếm một vai trò rất quan trọng của một tổ chức, công ty hay quốc gia. Trong Công nghệ thông tin vấn đề bảo mật được chú trọng và quan tâm một cách nghiêm túc. Đã có rất nhiều cơ chế bảo mật được đưa ra và thích hợp cho từng lĩnh vực riêng. Khóa luận tập trung nghiên cứu các vấn đề liên quan đến kiểm chứng cơ chế bảo mật thông tin dựa trên RBAC. Nghiên cứu các mô hình RBAC, các ví dụ về các mô hình và ứng dụng của các mô hình này trong thực tiễn. Giới thiệu công cụ CDT để xây dựng mô hình kiểm chứng cơ chế bảo mật dựa trên AST (Abstract Syntax Tree). Các ứng dụng của CDT trong bài toán kiểm chứng. Những nghiên cứu tập trung vào kiểm chứng mô hình RBAC dựa trên AST sẽ là nền móng cho những nghiên cứu rộng hơn và khả dụng hơn trong tương lai không xa. Để thuyết phục hơn, khóa luận đưa ra một bài toán ví dụ để kiểm chứng mô hình RBAC0 và mã nguồn viết bằng Java (trên công cụ Eclipse) và mô hình được Test trên ngôn ngữ C/C++. vii MỤC LỤC CHƯƠNG 1. GIỚI THIỆU .......................................................................... 1 1.1. Bối cảnh .......................................................................................................1 1.2. Mục tiêu khóa luận .....................................................................................1 1.3. Cấu trúc khóa luận .....................................................................................2 CHƯƠNG 2. CÁC MÔ HÌNH ĐIỀU KHIỂN TRUY CẬP DỰA TRÊN VAI TRÒ....................................................................................................... 3 2.1. Giới thiệu .....................................................................................................3 2.2. Nền tảng và động lực...................................................................................4 2.3. Các vai trò và các khái niệm liên quan ......................................................7 2.4. Các mô hình một họ tham chiếu.................................................................8 2.5. Mô hình cơ sở ............................................................................................10 2.6. Role có cấp bậc ..........................................................................................14 2.7. Các ràng buộc............................................................................................20 2.8. Mô hình hợp nhất......................................................................................24 2.9. Các mô hình quản lý .................................................................................26 2.10. Kết luận ...................................................................................................29 CHƯƠNG 3. GIỚI THIỆU CÔNG CỤ CDT TRONG ECLIPSE .......... 31 3.1. Tổng quan..................................................................................................31 3.2. Cấu trúc của CDT .....................................................................................31 3.3. Các tính năng của CDT ............................................................................32 3.4. Kết luận .....................................................................................................35 CHƯƠNG 4. BÀI TOÁN KIỂM CHỨNG................................................ 36 4.1. Giới thiệu:..................................................................................................36 4.2. Khái quát thuật toán .................................................................................36 4.3. Những khía cạnh liên quan.......................................................................38 4.3.1. Khía cạnh lý thuyết ......................................................................................38 4.3.2. Khía cạnh thực tiễn......................................................................................40 viii 4.4. Ứng dụng thuật toán .................................................................................41 4.4.1. Khái quát về ứng dụng ................................................................................41 4.4.2. Mục tiêu bài toán: ........................................................................................41 4.4.3. Yêu cầu bài toán: .........................................................................................42 4.4.4. Phân tích bài toán ........................................................................................42 4.5. Kết luận .....................................................................................................43 CHƯƠNG 5. THỰC NGHIỆM ................................................................. 45 5.1. Phạm vi ứng dụng .....................................................................................45 5.2. Thiết kế ứng dụng .....................................................................................45 5.3. Xây dựng và triển khai bài toán...............................................................48 5.3.1. Xây dựng chương trình chính .....................................................................48 5.3.2. Xây dựng chương trình kiểm tra: ...............................................................49 5.4. Kiểm thử chương trình .............................................................................53 5.4.1. Nội dung kiểm thử .......................................................................................53 5.4.2. Kết quả .........................................................................................................61 CHƯƠNG 6. KẾT LUẬN .......................................................................... 63 1 CHƯƠNG 1. GIỚI THIỆU 1.1. Bối cảnh Trong thời kỳ thông tin bùng nổ như hiện nay, tất cả các lĩnh vực trong đời sống xã hội đều sử dụng công nghệ thông tin như các cơ quan chính phủ, các ngân hàng hay các tổ chức.. Nhưng một thực tế đáng lo ngại là vấn đề bảo mật chưa được quan tâm thích đáng và chưa sử dụng hợp lý. Có rất nhiều cơ chế bảo mật được nghiên cứu và triển khai thích họp cho từng lĩnh vực khác nhau. Trong các mô hình đang tồn tại thì toàn diện nhất là RBAC. RBAC điều khiển việc truy cập dựa trên vai trò của từng người sử dụng. Mô hình này có nhiều ưu điểm, nhưng nội dung rất rộng nên khóa luận tập trung chuyên sâu vào mô hình đơn giản nhất và đặc trưng nhất của RBAC là RBAC0. 1.2. Mục tiêu khóa luận Khóa luận sẽ nghiên cứu những vấn đề sau: Khái niệm RBAC và đi vào chi tiêt các mô hình RBAC. Phần này giới thiệu một cách khái quát nhất RBAC là gì? Những đặc điểm, các mô hình và ứng dụng trong cơ chế bảo mật như thế nào? Sau khi tìm hiểu về RBAC, phần tiếp theo phát biểu bài toán kiểm chứng các mô hình của RBAC (cụ thể là RBAC0). Mã nguồn được biểu diễn dưới cấu trúc cây, phần này nêu lên thuật toán duyệt cây và đưa ra kết luận về tính đúng đắn của mã nguồn so với mô hình RBAC0. Khóa luận sẽ đề cập tới việc dùng Eclipse với công cụ CDT để sinh ra cây cú pháp trừu tượng (AST), cấu trúc AST và cách để duyệt nó. Mục tiêu quan trong của luận văn là lam sao đề xuất được một phương pháp hiệu quả để kiểm chứng mô hình RBAC0 với phần thực thi chương trình sử dụng AST 2 1.3. Cấu trúc khóa luận Khóa luận được cấu trúc như sau: Chương 2 phân tích chi tiết về các mô hình điều khiển truy cập dựa trên vai trò (RBAC). Các cách tiếp cận các mô hình của RBAC qua các ví dụ cụ thể Chương 3 giới thiệu về CDT - một công cụ để triển khai bài toán kiểm chứng. Giới thiệu trực quan qua các hình ảnh và các ứng dụng của thể của CDT. Chương này không nói hết về CDT chỉ đề cập các phần quan trọng nhất của CDT phục vụ trực tiếp cho khóa luận. Chương 4 nghiên cứu bài toán kiểm chứng và ứng dụng trên mô hình RBAC0. Từ cây cú pháp trừu tượng (AST) đưa ra thuật toán kiểm chứng có đầu vào là mã nguồn C/C++ và kết quả được so sánh với mô hình RBAC0 và kết luận về sự tương ứng của mô hình so với đoạn mã chuơng trình. Chương 5 là phần thực nghiệm sẽ cụ thể thuật toán đã đề cập ở chương 4 bằng cách đưa ra một bài toán cụ thể. Chương này sẽ đưa ra các chi tiết chạy chương trình và kết quả đạt được liên quan tới bài toán đang được nghiên cứu. Chương 6 là chương cuối nêu lên kết luận về khóa luận. 3 CHƯƠNG 2. CÁC MÔ HÌNH ĐIỀU KHIỂN TRUY CẬP DỰA TRÊN VAI TRÒ 2.1. Giới thiệu Khái niệm điều khiển truy cập dựa trên vai trò (RBAC) bắt đầu với hệ thống đa người sử dụng và đa ứng dụng trực tuyến được đưa ra lần đầu vào những năm 70. Ý tưởng trọng tâm của RBAC là permission (quyền hạn) được kết hợp với role (vai trò) và user (người sử dụng) được phân chia dựa theo các role thích hợp. Điều này làm đơn giản phần lớn việc quản lý những permission. Tạo ra các role cho các chức năng công việc khác nhau trong một tổ chức và user cũng được phân các role dựa vào trách nhiệm và trình độ của họ. Phân lại cho user từ chức năng này sang chức năng khác. Những role được cấp các permission mới vì các ứng dụng gắn kết chặt chẽ với các hệ thống và các permission được hủy khỏi các role khi cần thiết. Một role được xem như một kết cấu ngữ nghĩa mà cơ chế điều khiển truy cập đều hình thành xung quanh. Một tập hợp riêng biệt những user và các permission được lập ra bởi các role chỉ là tạm thời. Role ổn định hơn bởi vì hoạt động hay chức năng của một tổ chức thường ít thay đổi hơn. Một role tương ứng với một năng lực để làm một nhiệm vụ cụ thể, ví dụ một bác sỹ nội khoa hay một dựợc sỹ. Một role cũng là hiện thân của một thẩm quyền và một bổn phận như một giám sát dự án. Một thẩm quyền hay một trách nhiệm khác với một năng lực. Jane Doe có năng lực để điều hành một số bộ phận nhưng chỉ được phân công điều hành một bộ phận. Các role phản ánh cho các nhiệm vụ được phân công cụ thể được luân phiên giữa nhiều user, ví dụ công việc của một bác sỹ nội khoa hay một quản lí ca. Các mô hình RBAC và sự cài đặt nên có khả năng cải thiện cung cấp tất cả các biểu hiện của khái niệm role. Theo một nghiên cứu mới đây của NIST [1] thì RBAC nhằm vào nhu cầu của các ngành kinh doanh hay của cả chính phủ. Trong công trình nghiên cứu của 28 tổ chức này, 4 nhu cầu điều khiển truy cập bị chi phối bởi nhiều mối quan tâm khác nhau gồm cả người tiêu dùng, cổ đông và sự tin cậy của các công ty bảo hiểm, sự riêng tư của thông tin cá nhân, việc ngăn chặn sự phân bố tài sản tài chính trái phép, ngăn chặn sử dụng không phép các đường dây điện thoại đường dài và sự giữ vững các tiêu chuẩn nghề nghiệp. Nhiều tổ chức đưa ra các quyết định điều khiển truy cập dựa trên role mà user là cá nhân đảm nhận như một bộ phận của tổ chức. Nhiều tổ chức thích kiểm soát tập trung và duy trì quyền truy cập, không theo ý muốn cá nhân của người quản lí hệ thống lắm mà theo các chỉ dẫn bảo vệ của tổ chức. Bản nghiên cứu cho thấy các tổ chức thường xem các nhu cầu điều khiển truy cập của họ là duy nhất và cảm thấy các sản phẩm có sẵn thiếu sự linh hoạt. Các role được xem như một phần của tiêu chuẩn SQL3 nổi bật cho hệ thống quản lí dữ liệu, dựa vào sự thực hiện của chúng trong Oracle 7. Các role được kết nối chặt chẽ trong hiện trạng an ninh thương mại. RBAC cũng phù hợp với công nghệ đang thịnh hành và các xu hướng kinh doanh. Một loạt sản phẩm cung cấp trực tiếp một dạng RBAC, các sản phẩm khác hỗ trợ những tính năng có liên quan chặt chẽ, ví dụ nhóm user, những tính năng này được sử dụng để thực hiện các role. 2.2. Nền tảng và động lực Mục đích chính của RBAC làm cho việc quản trị an ninh và xem lại thuận tiện hơn. Nhiều hệ thống kiểm soát truy cập cho các máy tính lớn thành công về thương mại thực hiện role quản trị an ninh. Ví dụ, role là người vận hành có thể truy cập tất cả các tài nguyên mà không thay đổi các quyền truy cập, role là một nhân viên bảo vệ có thể thay đổi các quyền truy cập nhưng không được truy cập vào các tài nguyên, và role là một kiểm toán viên có thể truy cập vào các đường kiểm toán. Việc sử dụng các role mang tính quản lí này cũng đựợc có trong các hệ thống điều khiển mạng hiện đại như Novell’s NetWare và Microsoft Windows NT. Sự quan tâm mới xuất hiện trở lại đây đối với RBAC tập trung chủ yếu vào khả năng sử dụng RBAC ở cấp độ ứng dụng. Trong quá khứ và cả ngày nay, các ứng dụng 5 đặc biệt đã được xây dựng với RBAC được mã hóa trong bản thân sự ứng dụng. Các hệ điều hành hiện có và các môi trường cung cấp rất ít khả năng sử dụng RBAC ở cấp độ ứng dụng. Khả năng này bây giờ bắt đầu xuất hiện trong các sản phẩm. Thách thức đặt ra là phải xác định được ứng dụng độc lập tiện lợi khá linh hoạttất nhiên dễ dàng thực hiện, sử dụng và hỗ trợ nhiều ứng dụng với sự điều chỉnh nhỏ nhất. Các biến thể tinh vi của RBAC bao gồm khả năng thiết lập mối quan hệ giữa các role cũng như là giữa các permission và các role và giữa các user với các role. Ví dụ, hai role có thể đươc lập sao cho loại trừ nhau do đó cùng một user không đựơc phép thực hiện cả hai role. Các role cũng có thể có quan hệ kế thừa, theo đó một role kế thừa các permission được gắn cho role khác. Những mối quan hệ role – role này có thể được sử dụng để làm cho các chính sách bảo mật bao gồm sự tách rời các công việc và sự ủy thác của người có thẩm quyền. Từ trước đến nay những mối quan hệ này đựợc mã hóa trong phần mềm ứng dụng, với RBAC, chúng đựợc định rõ một lần cho một miền bảo mật. Với RBAC, người ta có thể xác định được các mối quan hệ role – permission. Điều này giúp cho việc gán cho các user tới các role xác định dễ dàng. Bản nghiên cứu NIST [1] chỉ ra rằng các permission được phân cho các role có xu hướng thay đổi tương đối chậm so với sự thay đổi thành viên những user các role. Nghiên cứu này cũng đã nhận thấy việc cho phép các quản trị viên cấp hoặc hủy bỏ tư cách thành viên của các user trong các role đang tồn tại mà không cho các quản trị viên này quyền tạo role mới hay thay đổi sự phân chia role – permission là điều đang đựợc mong muốn. Việc phân công các user theo role sẽ cần ít kĩ năng kĩ thuật hơn việc phân công các permission theo role. Nếu không có RBAC, việc xác định permission nào được ủy thác cho user nào sẽ khó. Chính sách điều khiển truy cập được thể hiện ở các thành tố khác nhau của RBAC như mối quan hệ role – permission, mối quan hệ user – role và mối quan hệ role – role. Những thành tố này cùng xác định xem liệu một user cụ thể có được phép truy cập vào 6 môt mảng dữ liệu trong hệ thống hay không. Các thành tố RBAC có thể đựợc định dạng trực tiếp bởi người sở hữu hệ thống hay gián tiếp bởi các role thích hợp mà người sở hữu hệ thống ủy thác. Chính sách có hiệu lực trong một hệ cụ thể nào đó là kết quả cuối cùng của việc định dạng các thành tố RBAC khác nhau một cách trực tiếp bởi người sở hữu hệ thống. Ngoài ra chính sách điều khiển truy cập có thể gia tăng trong chu kì của hệ thống và ở các hệ lớn điều này là chắc chắn xảy ra. Khả năng biến đổi chính sách để đáp ứng được nhu cầu đang thay đổi của một tổ chức là một lợi ích quan trọng của RBAC. Mặc dù RBAC là một chính sách trung lập, nó trực tiếp hỗ trợ ba nguyên tắc bảo mật nổi tiếng: đặc quyền ít nhất, sự tách biệt các nhiệm vụ, trừu tượng hóa dữ liệu. Nguyên tắc đặc quyền ít nhất đựợc hỗ trợ vì RBAC được định dạng do đó chỉ những permission mà nhiệm vụ do các thành viên của role quản lí đó cần mới được phân cho role đó. Sự tách biệt các nhiệm vụ đạt được bằng cách đảm bảo những role có quan hệ loại trừ lẫn nhau phải đựơc sử dụng tới để hoàn thành một công việc nhạy cảm như yêu cầu một nhân viên kế toán và một quản lí kế toán tham gia vào phát hành một tấm Sec. Trừu tượng hóa dữ liệu được hỗ trợ bằng các permission trừu tượng như credit (bên có) và debit (bên nợ) cho một tài khoản, chứ không phải là các permission đọc, viết, quản lí thường đựợc hệ điều hành cung cấp. Tuy nhiên, RBAC không cho phép ứng dụng các nguyên lý này. Nhân viên bảo mật có thể định dạng được RBAC do đó nó vi phạm những nguyên lí này. Ngoài ra, mức độ trừu tuợng hóa dữ liệu đựợc hỗ trợ sẽ do các chi tiết bổ sung quyết định. RBAC không phải là giải pháp cho mọi vấn để kiểm soát truy cập. Người ta cần những dạng kiểm soát truy cập phức tạp hơn khi xử lí các tình huống mà trong đó chuỗi các thao tác cần được kiểm soát. Ví dụ, một lệnh mua cần nhiều bước trước khi đơn dặt hàng mua được phát hành. RBAC không cố kiểm soát trực tiếp các permission cho một chuỗi các sự kiện như vậy. Các dạng khác của kiểm soát truy cập đựợc cài đặt trên bề mặt RBAC vì mục đích này. Việc kiểm soát một chuỗi các thao tác ngoài