Đăng ký Đăng nhập
Trang chủ Nghiên cứu kỹ thuật giải thích trừu tượng...

Tài liệu Nghiên cứu kỹ thuật giải thích trừu tượng

.PDF
90
130
143

Mô tả:

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN ------------------- NGUYỄN THANH LIÊM NGHIÊN CỨU KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG LUẬN VĂN THẠC SĨ KHOA HỌC Hà Nội – Năm 2014 ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC KHOA HỌC TỰ NHIÊN ------------------- NGUYỄN THANH LIÊM NGHIÊN CỨU KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG Chuyên ngành: CƠ SỞ TOÁN HỌC CHO TIN HỌC Mã số: 60460110 LUẬN VĂN THẠC SĨ KHOA HỌC NGƯỜI HƯỚNG DẪN KHOA HỌC TS. NGUYỄN TRƯỜNG THẮNG Hà Nội – Năm 2014 LỜI CAM ĐOAN Tôi xin cam đoan đây là công trình nghiên cứu của tôi trong đó có sự giúp đỡ của giáo viên hướng dẫn TS. Nguyễn Trường Thắng - Viện Công nghệ thông tin – Viên Hàn lâm Khoa học và Công nghệ Việt Nam. Các nội dung và kết quả nghiên cứu trong luận văn này là hoàn toàn trung thực, được tham khảo theo các tài liệu của các tác giả do giáo viên hướng dẫn cung cấp và được liệt kê tại mục tài liệu tham khảo. Học viên Nguyễn Thanh Liêm 1 LỜI CẢM ƠN Lời đầu tiên tôi xin gửi lời cảm ơn chân thành và bày tỏ lòng biết ơn sâu sắc nhất tới giáo viên hướng dẫn TS. Nguyễn Trường Thắng – Phó Viện trưởng - Viện Công nghệ thông tin - Viện Hàn lâm Khoa học và Công nghệ Việt Nam, thầy đã hướng dẫn tận tình, giúp đỡ và truyền đạt cho những kiến thức, kinh nghiệm quí báu trong suốt thời gian vừa qua, thầy đã cung cấp cho tôi các tài liệu rất hữu ích để hoàn thành luận văn này. Tôi cũng xin gửi lời cảm ơn chân thành tới tất cả các thầy, cô trong bộ môn Tin học - Khoa Toán - Cơ - Tin học - Trường Đại học Khoa học Tự nhiên - ĐHQG Hà Nội đã giúp đỡ tôi về kiến thức, tinh thần và những lời khuyên quí báu trong suốt quá trình học tập vừa qua. Cảm ơn đến tất cả các bạn bè, đồng nghiệp trong Viện Công nghệ thông tin - Viện Hàn lâm Khoa học và Công nghệ Việt Nam, trường Đại học Hải Dương đã cung cấp cho tôi những tài liệu quí báu, giúp đỡ, động viên và tạo điều kiện cho tôi về tất cả mọi mặt trong suốt một năm qua. Cuối cùng tôi xin gửi lời cảm ơn tới các thành viên trong gia đình đã tạo điều kiện tốt nhất cho tôi, động viên, cổ vũ tôi trong quá trình học tập và nghiên cứu để tôi hoàn thành luận văn này. Học viên Nguyễn Thanh Liêm 2 MỤC LỤC LỜI CAM ĐOAN ............................................................................................. 1 LỜI CẢM ƠN ................................................................................................... 2 MỤC LỤC ......................................................................................................... 3 DANH MỤC CÁC THUẬT NGỮ VÀ CHỮ VIẾT TẮT ................................ 6 DANH MỤC CÁC HÌNH VẼ .......................................................................... 7 MỞ ĐẦU ........................................................................................................... 8 Chương 1 - TỔNG QUAN .............................................................................. 10 1.1. Tổng quan về phân tích chương trình .................................................. 10 1.1.1. Ý tưởng của bài toán phân tích chương trình ............................... 11 1.1.2. Phân tích chương trình tĩnh ........................................................... 12 1.2. Tổng quan về kỹ thuật giải thích trừu tượng........................................ 13 1.3. Tổng quan về tình hình nghiên cứu ..................................................... 15 1.4. Kết luận chương 1 ................................................................................ 16 Chương 2 - CỞ SỞ LÝ THUYẾT CỦA KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG ........................................................................................................... 17 2.1. Khái niệm về kỹ thuật giải thích trừu tượng ........................................ 17 2.2. Ứng dụng của kỹ thuật giải thích trừu tượng ....................................... 17 2.3. Một số khái niệm cơ bản ...................................................................... 18 2.3.1. Ngữ nghĩa cụ thể của chương trình ............................................... 18 2.3.2. Thuộc tính an toàn của chương trình ............................................ 19 2.3.3. Miền trừu tượng ............................................................................ 20 2.3.4. Độ phủ của kỹ thuật giải thích trừu tượng .................................... 21 2.3.5. Các phương pháp hình thức .......................................................... 22 2.3.6. Tính chất cần thiết của ngữ nghĩa trừu tượng ............................... 23 2.4. Lý thuyết dàn........................................................................................ 25 3 2.5. Lý thuyết điểm cố định ........................................................................ 28 2.5.1. Điểm cố định ................................................................................. 28 2.5.2. Mở rộng ký hiệu điểm cố định ...................................................... 29 2.5.3. Bước lặp ........................................................................................ 29 2.5.4. Đồ thị luồng điều khiển (Control Flow Graphs - CFG)................ 33 2.5.5. Phân tích luồng dữ liệu (Data Flow Analysis) .............................. 36 2.5.6. Thuật toán tìm điểm cố định ......................................................... 36 2.6. Tiếp cận kết nối Galois cho kỹ thuật giải thích trừu tượng ................. 38 2.6.1. Kết nối Galois ............................................................................... 38 2.6.2. Tính đủ và tính chính xác (Soundness and Precision) .................. 39 2.6.3. Mở rộng tới không gian hàm (Extension to Function Spaces) ..... 40 2.6.4. Trừu tượng hàm (Functional Abstraction) .................................... 41 2.7. Trừu tượng hóa ngữ nghĩa chương trình .............................................. 41 2.7.1. Hệ dịch chuyển.............................................................................. 41 2.7.2. Ngữ nghĩa vết (Trace semantics) .................................................. 43 2.7.3. Biểu diễn ngữ nghĩa vết dưới dạng điểm cố định ......................... 44 2.7.4. Bao đóng phản xạ bắc cầu (RTC - reflexive transitive closure) là trừu tượng hóa của ngữ nghĩa vết ........................................................... 45 2.7.5. Thỏa mãn kết nối Galois ............................................................... 45 2.7.6. Biểu diễn ngữ nghĩa RTC dưới dạng điểm cố định ...................... 46 2.7.7. Ngữ nghĩa tới được là trừu tượng hoá của ngữ nghĩa RTC .......... 47 2.7.8. Biểu diễn ngữ nghĩa tới được dưới dạng điểm cố định ................ 47 2.8. Kết luận chương 2 ................................................................................ 48 Chương 3 - THỰC NGHIỆM ......................................................................... 49 3.1. Giới thiệu về TVLA ............................................................................. 49 3.2. Phân tích trong TVLA.......................................................................... 50 4 3.2.1. Cấu trúc 3-valued Logic ................................................................ 51 3.2.2. Biểu diễn trạng thái bộ nhớ Heap qua cấu trúc Logic .................. 52 3.2.3. Trừu tượng heap ............................................................................ 53 3.2.4. Biểu diễn ngữ nghĩa và chương trình ............................................ 55 3.2.5. Ví dụ về phân tích chương trình ................................................... 57 3.3. Thuật toán sinh hệ ràng buộc Coerce và thuật toán giải hệ ràng buộc tìm điểm cố định Focus ............................................................................... 59 3.3.1. Công thức ...................................................................................... 59 3.3.2. Các lớp con của công thức ............................................................ 60 3.3.3. Ngữ nghĩa ...................................................................................... 60 3.3.4. Focus ............................................................................................. 61 3.3.5 Công thức cập nhật......................................................................... 63 3.3.6. Thuật toán Coerce xác định hệ ràng buộc..................................... 65 3.3.7. Thuật toán Focus giải hệ ràng buộc .............................................. 67 3.4. Thử nghiệm .......................................................................................... 70 3.4.1. Đặc tả hệ thống trong TVLA ............................................................ 70 3.4.2. Giới thiệu bài toán ......................................................................... 71 3.4.3. Đặc tả dữ liệu đầu vào................................................................... 71 3.4.4. Kết quả phân tích .......................................................................... 76 3.5. Kết luận chương 3 ................................................................................ 77 KẾT LUẬN ..................................................................................................... 78 TÀI LIỆU THAM KHẢO ............................................................................... 79 PHỤ LỤC A: ................................................................................................... 81 PHỤ LỤC B: ................................................................................................... 83 5 DANH MỤC CÁC THUẬT NGỮ VÀ CHỮ VIẾT TẮT TT Tiếng Anh - Viết tắt 1 Abstract domain Tiếng Việt Miền trừu tượng 2 Abstract semantics Ngữ nghĩa trừu tượng 3 Concrete domain Miền cụ thể 4 Concrete semantics Ngữ nghĩa cụ thể 5 Continue - con Tính liên tục của một hàm số 6 Control Flow Graphs - CFG Đồ thị luồng điều khiển 7 Data Flow Analysis - DFA Phân tích luồng dữ liệu 8 Fixpoint - fix 9 Fixpoint approximation 10 Galois connections Điểm cố định Xấp xỉ điểm cố định Kết nối Galois 11 Interval semantics Ngữ nghĩa khoảng Dàn - Tập hợp các phần tử có thứ tự từng phần có điểm chặn dưới lớn nhất và trặn trên nhỏ nhất Tính đơn điệu của một hàm Thu hẹp Tập hợp các phần tử có thứ tự Tính chính xác Ngữ nghĩa tới được 12 Lattice 13 14 15 16 17 Monotone - mon Narrowing Partial Ordered Set - Poset Precise Reachability semantics 18 Reflexive transitive closure - RTC Reflexive transitive closure 19 semantics - RTCs 20 Soundness Bao đóng phản xạ bắc cầu Ngữ nghĩa bao đóng phản xạ bắc cầu Tính đủ 21 Trace semantics Ngữ nghĩa vết, Tập hợp các dấu vết về quá trình chuyển đổi trạng thái của chương trình. 22 Transition system 23 Widening Hệ dịch chuyển Mở rộng 6 DANH MỤC CÁC HÌNH VẼ TT 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 Hình ảnh sử dụng Hình 1.1: Bài toán phân tích chương trình tổng quát Hình 1.2: Trừu tượng hóa theo điểm cố định Hình 1.3: Các thành phần chính của phân tích chương trình Hình 2.1 Sơ đồ hành vi có thể của chương trình Hình 2.2: Quĩ đạo an toàn của các thực thi Hình 2.3: Quĩ đạo không an toàn đối với kiểm thử/gỡ lỗi Hình 2.4: Biểu diễn miền trừu tượng Hình 2.5: Trừu tượng hóa quĩ đạo hành vi của chương trình Hình 2.6: Trừu tượng hóa quĩ đạo hành vi không đảm bảo tính đủ Hình 2.7: Lỗi trừu tượng hóa quĩ đạo hành vi không chính xác Hình 2.8: Tiêu chuẩn trừu tượng hóa theo khoảng Hình 2.9: Biểu đồ Hasse của dàn (2A,⊆) Hình 2.10: Biểu diễn ngữ nghĩa của một chương trình thành dàn Hình 2.11: Biểu diễn điểm cố định của hàm cosx = x Hình 2.12: Tính toán điểm cố định trên dàn Hình 2.13: Phép cộng dàn Hình 2.14: Phép nâng dàn Hình 2.15: Dàn phẳng Hình 2.16: CFG cho các lệnh đơn giản Hình 2.17: CFG cho cấu trúc tuần tự Hình 2.18: CFG cho cấu trúc rẽ nhánh Hình 2.19: CFG cho cấu trúc lặp Hình 2.20: CFG của hàm tính n! Hình 2.21: ¯F(¯x) là một xấp xỉ của F(x) Hình 2.22: Biểu diễn quan hệ chuyển tiếp ngữ nghĩa chương trình Hình 2.23: Hệ chuyển dịch quĩ đạo thực thực thi của chương trình Hình 2.24: Biểu diễn ngữ nghĩa vết thực thi Hình 2.25: Biểu diễn ngữ nghĩa vết dưới dạng điểm cố định Hình 2.26: Trừu tượng hóa đến ngữ nghĩa tới được Hình 3.1: Các toán tử 3-valued logic của Kleene Hình 3.2: Biểu diễn heap cụ thể Hình 3.3: Trừu tượng hóa heap Hình 3.4: Kết quả heap trừu tượng đầu ra Hình 3.5: Trạng thái của chương trình sử dụng cấu trúc 2-valued logic Hình 3.6: Trạng thái của chương trình sử dụng 3-valued logic Hình 3.7: Biểu diễn quá trình làm việc của phân tích chương trình Hình 3.8: Ứng dụng của giải thích trừu tượng cho phân tích lệnh Hình 3.9: Kết quả phân tích hàm tạo danh sách liên kết 7 Trang 12 14 14 18 19 20 21 22 24 24 25 26 28 30 30 32 31 32 34 34 34 35 35 41 42 42 43 44 48 52 53 55 56 58 58 59 62 77 MỞ ĐẦU Ngày nay, các hệ thống phần mềm được sử dụng một cách phổ biến trên tất cả các lĩnh vực của đời sống, trong sản xuất, kinh doanh như: kinh tế, tài chính, kế toán, y tế, giáo dục, chính phủ,… , và trong các thiết bị điện tử công nghiệp và dân dụng, nó được phát triển trở lên ngày càng phức tạp. Sự phức tạp này còn lớn hơn đối với các hệ thống điều khiển và các hệ thống nhúng trong các thiết bị công nghiệp, hàng không, vũ trụ, … Đối với những đơn vị, cá nhân và các tổ chức làm phần mềm chuyên nghiệp họ đều hiểu rằng một sản phẩm phần mềm được họ tạo ra không thể nào chạy một cách hoàn hảo ngay từ lúc đầu tiên mà không mắc bất kỳ một lỗi gì. Trong quá trình phát triển và đưa vào sử dụng một phần mềm bất kỳ, thì hầu hết tất cả các lỗi chỉ được phát hiện sau khi phần mềm đó được đưa vào sử dụng. Do vậy, các hoạt động kiểm thử đóng góp một vai trò rất quan trọng nhằm đảm bảo chất lượng của các hệ thống phần mềm. Các hoạt động kiểm thử này luôn được các nhà phát triển phần mềm tính đến trong suốt quá trình phát triển cho một hệ thống phần mềm. Tuy nhiên, các hoạt động kiểm thử thường có chi phí rất cao, nó chiếm đến 40% toàn bộ chi phí phát triển phần mềm, còn về mặt thời gian thì đôi khi nó còn nhiều hơn cả việc xây dựng hệ thống. Hầu hết các hoạt động kiểm thử nhằm mục đích phân tích các thành phần và cấu trúc của phần mềm để xác định số lượng lớn nhất các lỗi trong tiến trình phát triển: từ đặc tả cho đến mã hóa. Đối với các hệ thống phần mềm phức tạp, cách giải quyết đưa ra ban đầu với các hệ thống bao giờ cũng là cẩn thận trong từng khâu: phân tích, thiết kế, lập trình, kiểm thử để giảm thiểu một cách tối đa các lỗi phát sinh. Các nguồn lực cần thiết cho hoạt động kiểm thử là rất quan trọng. Vì vậy, việc nghiên cứu các phương pháp nhằm mục đích giảm chi phí trong quá trình kiểm thử đã được đưa ra, nhưng vẫn đảm bảo mục tiêu về tính hiệu quả của phần mềm là một biện pháp hữu hiệu. 8 Do vậy, trong luận văn này tôi giới thiệu một phương pháp trong lĩnh vực phân tích chương trình tĩnh. Cụ thể là nghiên cứu về kỹ thuật giải thích trừu tượng, mục tiêu chính là cập nhật các xu hướng mới của kỹ thuật này ở trên thế giới để nâng cao chất lượng phần mềm. Các đề tài nghiên cứu về kỹ thuật giải thích trừu tượng chưa được phổ biến ở trong nước, do vậy trong khuôn khổ của đề tài tôi xin trình bày các khái niệm cơ bản, cơ sở lý thuyết ban đầu dựa trên các báo cáo tại các hội nghị thường niên VMCAI (Verification, Model Checking, and Abstract Interpretation) và các tài liệu nghiên cứu, bài giảng của tác giả Patrick Cousot trong những năm gần đây. Ứng dụng thử nghiệm tập trung vào công cụ mã nguồn mở TVLA (3 – Valued Logic Analysis Engine) được phát triển bởi Lev-Ami trường Đại học Khoa học Máy tính Tel Aviv – Israel. Bố cục của luận văn gồm 3 chương: Chương 1 - TỔNG QUAN: Tập trung vào các khái niệm liên quan đến kiểm chứng phần mềm, phân tích chương trình tĩnh, tiếp cận lý thuyết của kỹ thuật giải thích trừu tượng trong phân tích chương trình tĩnh, tình hình nghiên cứu ở trong và ngoài nước. Chương 2 - CƠ SỞ LÝ THUYẾT CỦA KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG: Tập trung vào cơ sở lý thuyết toán học của kỹ thuật giải thích trừu tượng, các phương pháp trừu tượng hóa ngữ nghĩa chương trình, biểu diễn ngữ nghĩa của chương trình thông qua các kỹ thuật trừu tượng, …, và ứng dụng trong kỹ thuật giải thích trừu tượng. Chương 3 - THỬ NGHIỆM: Tập trung vào việc cài đặt phương pháp phân tích chương trình tĩnh bằng kỹ thuật giải thích trừu tượng dựa trên bộ công cụ mã nguồn mở TVLA, làm rõ các ứng dụng trong phân tích hình dạng. KẾT LUẬN: Trình bày nội dung nghiên cứu đã đạt được, các hạn chế trong quá trình nghiên cứu và định hướng nghiên cứ tiếp theo. 9 Chương 1 - TỔNG QUAN 1.1. Tổng quan về phân tích chương trình Sự phát triển vượt bậc, nhanh chóng của các thiết bị phần cứng với một hệ số 106 lần trong gần 40 năm qua đã dẫn đến sự bùng nổ của kích cỡ các chương trình phần mềm cũng theo một tỉ lệ tương tự chạy trên chúng. Về Qui mô và phạm vi của các chương trình ứng dụng cực lớn này (từ 1 tới 40 triệu dòng mã lệnh) có thể vẫn tiếp tục mở rộng nhanh chóng trong thập kỉ tới. Các chương trình cực lớn như vậy sẽ phải được thiết kế với chi phí hợp lý, theo sau đó vẫn phải sửa chữa, bảo trì và nâng cấp trong suốt dòng đời của chúng (thông thường là khoảng trên 20 năm). Trên thực tế là số lượng và hiệu quả của các đội lập trình, phụ trách việc bảo trì, theo dõi chúng không thể phát triển theo tỷ lệ tương tự như vậy. Trong điều kiện như vậy, một tỉ lệ không quá hiếm gặp với 1 lỗi trong 1000 dòng mã lệnh đối với những chương trình cực lớn này thường là quá lạc quan và sẽ không thể nhanh chóng đạt được trong một tương lai gần (hầu như không thể kiểm soát được), đặc biệt đối với những hệ thống quan trọng đòi hỏi độ an toàn cao. Vì vậy trong khoảng 10 năm tới, vấn đề về độ tin cậy của phần mềm (software reliability) có một khả năng sẽ trở thành là một mối quan tâm rất lớn và cũng là một thách thức rất lớn đối với một xã hội hiện đại phụ thuộc rất nhiều vào máy tính [7]. Trong hơn 3 thập kỷ qua, rất nhiều tiến bộ đã được thực hiện cả về mặt tư duy/công cụ hỗ trợ (để nâng cao khả năng về trí tuệ của con người) để ứng phó với các hệ thống phần mềm phức tạp giúp cho các lập trình viên suy luận tốt hơn về chương trình [7]. Rất nhiều các kỹ thuật kiểm chứng phần mềm (software verification) và các công cụ hỗ trợ kèm theo đã được phát triển, bắt đầu bằng các thực hiện/ mô phỏng chương trình trong nhiều môi trường khác nhau có thể. Tuy nhiên, gỡ lỗi mã biên dịch hoặc mô hình mô phỏng của mã nguồn chương trình là 10 hầu như không thể mở rộng về qui mô và thường chỉ đưa ra được một phạm vi bao phủ thấp các hành vi động của chương trình. Các phương pháp hình thức (formal methods) trong kiểm chứng chương trình (program verification) đã rất lỗ lực trong việc chứng minh một cách tự động rằng chương trình sẽ thực hiện là chính xác trong tất cả các môi trường đặc tả. Lĩnh vực nghiên cứu này bao gồm các phương pháp suy diễn (diductive methods), kiểm chứng mô hình (model checking), định kiểu chương trình (program typing) và phân tích chương trình tĩnh (static program analysis) [7]. Khi bài toán kiểm chứng chương trình đã được chứng minh là không giải được. Vì vậy, việc hỗ trợ tính toán cho tất cả các phương pháp kiểm chứng là không hoàn chỉnh (incomplete). Độ phức tạp tính toán hoặc tính không giải được này sẽ được giải quyết bằng cách sử dụng một số hình thức xấp xỉ với mục đích là đưa chúng về bài toán giải được hoặc làm giảm độ phức tạp tính toán trong quá trình kiểm chứng chương trình [7]. 1.1.1. Ý tưởng của bài toán phân tích chương trình Bài toán phân tích chương trình tĩnh có thể được mô tả như sau: Cho trước một chương trình và một đặc tả , phân tích chương trình sẽ kiểm tra xem ngữ nghĩa của chương trình L có thỏa mãn đặc S hay không (minh họa hình 1.1). Trong trường hợp xảy ra lỗi, quá trình phân tích sẽ cung cấp các gợi ý để tìm hiểu nguồn gốc của lỗi (bằng cách phân tích ngược lại sẽ cung cấp các điều kiện cần thiết cho đặc tả thông qua phản ví dụ) [7]. Ví dụ 1.1: Cho đoạn chương trình cần phân tích như sau: 1. a = 0; 2. while(a < 1000){ 3. a = a + 1; 4. } 5. return; L là mã nguồn và S là giá trị của biến 11 ∈ [0,1000]. Hình 1.1: Bài toán phân tích chương trình tổng quát 1.1.2. Phân tích chương trình tĩnh Phân tích chương trình tĩnh là việc xác định tĩnh tự động các thuộc tính động về thời gian thực thi của chương trình. Có rất nhiều câu hỏi thú vị mà người ta có thể được hỏi về một chương trình nhất định nào đó: + Chương trình hiện tại có dừng hay không? + Độ lớn của vùng nhớ (heap) là bao nhiêu trong quá trình thực thi? + Đầu ra có thể của nó là gì? Các câu hỏi khác liên quan đến các điểm chương trình riêng lẻ trong mã nguồn cũng được đưa ra: + Biến x luôn luôn có giá trị như nhau hay không? + Giá trị của x sẽ được đọc trong tương lai hay không? + Có thể con trỏ p là null không? + Các biến p có thể trỏ đến vùng nhớ nào? + Biến x có được khởi tạo trước khi nó được đọc hay không? + Giá trị của biến số nguyên x là luôn dương? 12 + Các ràng buộc trên và ràng buộc dưới là như thế nào đối với giá trị của biến số nguyên x? + … Theo lý thuyết Rice (một kết quả tổng quát từ năm 1953) có thể được giải thích rằng tất cả các câu hỏi thú vị nêu trên về hành vi của chương trình là không giải được, điều này rất dễ dàng thấy trong bất kỳ trường hợp đặc biệt nào [2]. 1.2. Tổng quan về kỹ thuật giải thích trừu tượng Nguyên tắc của kỹ thuật giải thích trừu tượng (abstract interpretation) là dựa trên tính toán xấp xỉ ngữ nghĩa của chương trình nhằm mục đích kiểm tra sự thỏa mãn một đặc tả nhất định. Kỹ thuật này được sử dụng để suy ra từ một ngữ nghĩa chuẩn (standard semantics) trên miền cụ thể (concrete domain) được một ngữ nghĩa trừu tượng (abstract semantics), ngữ nghĩa này đã được xấp xỉ và tính toán được (approximate and computable abstract semantics) trên miền trừu tượng (abstract domain) theo hình minh họa 1.2 [7]. Tuy nhiên với quá trình suy dẫn này, bản thân nó không hoàn toàn tự động mà có thể cần sự tương tác với người dùng để tinh chỉnh (refinement), các hàm trừu tượng tạo ra thông qua các tham số đưa vào, bởi vì có thể đầu tiên (là ngữ nghĩa trừu tượng từ L) không thỏa mãn đặc tả S, khi đó ta không kết luận ngay là chương trình L không thỏa mãn đặc tả S do tính không hoàn chỉnh (incompleteness) của kỹ thuật giải thích trừu tượng trước hết phải tinh chỉnh lại hàm của L, mà sao cho phù hợp. Nếu S thỏa mãn bởi , do tính đúng đắn của kỹ thuật giải thích trừu tượng suy ra S thỏa mãn L. Ưu điểm lớn nhất của kỹ thuật này là độ phức tạp tính toán trên nhỏ hơn rất nhiều so với L tùy theo quá trình trừu tượng hóa (hàm trừu tượng hóa từ L vào ), được minh họa trong hình 1.2: 13 Hình 1.2: Trừu tượng hóa theo điểm cố định ⊑ ( # ) Trong thực tế, việc phân tích chương trình tĩnh bằng kỹ thuật giải thích trừu tượng có chứa một thành phần là bộ sinh (generator) ngữ nghĩa trừu tượng thông qua việc đọc mã nguồn chương trình và tạo ra các hệ phương trình điểm cố định hoặc hệ phương trình ràng buộc cần giải bởi máy tính, thành phần tiếp theo của kỹ thuật này là bộ giải (solver) được sử dụng để giải các hệ phương trình điểm cố định/hệ phương trình ràng buộc. Các thành phần chính của kỹ thuật này được mô tả trong hình 1.3 [7]. Hình 1.3: Các thành phần chính của phân tích chương trình 14 Khi tìm được nghiệm xấp xỉ của hệ, một phương pháp phổ biến là dùng hàm lặp khi giải. Các khái niệm và kỹ thuật trừu tượng hóa sẽ được xem xét trong chương 2, việc tìm nghiệm thông qua hàm lặp có hạn chế về mặt thời gian (phương pháp không hội tụ sau vô hạn lần lặp), nếu giới hạn của hàm lặp là không tồn tại (trường hợp này là có thể, ví dụ như khái niệm trừu tượng theo đa diện) hoặc nó đạt được giới hạn sau vô hạn bước lặp (ví dụ trừu tường tượng hóa phân khoảng và bát giác), sự hội tụ này có thể được đảm bảo hoặc/và tăng tốc độ hội tụ bằng cách sử dụng một số kỹ thuật mở rộng để mở rộng hơn các ước lượng nghiệm gần đúng trong hữu hạn các bước tiếp theo bởi một kỹ thuật thu hẹp để cải thiện nó [7]. Trong khuôn khổ mà luận văn trình bày sẽ không đề cập đến các kỹ thuật liên quan đến trừu tượng phân khoảng, trừu tượng bát giác, trừu tượng đa diện cũng như các kỹ thuật liên quan đến mở rộng, thu hẹp điểm cố định. 1.3. Tổng quan về tình hình nghiên cứu Khảo sát ở trong nước: Hiện nay ở Việt Nam việc sử dụng các phương pháp hình thức trong thực tế kiểm chứng phần mềm còn nhiều hạn chế. Trong 3 mảng: phương pháp suy diễn (deductive method), kiểm chứng mô hình (model checking) và phân tích tĩnh với giải thích trừu tượng (static analysis with abstract interpretation) thì mảng phân tích tĩnh với giải thích trừu tượng có nhiều lợi thế khi sử dụng thực tế, với khả năng tự động sinh được mô hình ngữ nghĩa trừu tượng từ mã nguồn để kiểm chứng và có thể áp dụng cho các hệ thống vô hạn trạng thái. Tuy nhiên, đây lại là mảng chưa nhận được nhiều sự quan tâm nghiên cứu như hai mảng còn lại. Có rất ít đề tài nghiên cứu về ứng dụng kỹ thuật giải thích trừu tượng trong phân tích chương trình, các đề tài nghiên cứu tập trung chủ yếu ở Viện Công nghệ thông tin - Viện Hàn lâm Khoa học và Công nghệ Việt Nam, Đại học Quốc gia Hà Nội, Đại học Bách khoa Đà Nẵng và Đại học Quốc gia Thành phố Hồ Chí Minh. 15 Khảo sát ở nước ngoài: tham khảo các kết quả của tác giả chính Patrick Cousot, và những báo cáo tại các hội nghị thường niên VMCAI (Verification, Model Checking, and Abstract Interpretation) trong những năm gần đây. Ứng dụng kỹ thuật giải thích trừu tượng trong phân tích chương trình tĩnh tập trung vào hai mảng lớn: phân tích luồng dữ liệu (Data-flow Analysis) và phân tích dựa trên tập hợp (Set-based Analysis) [8]. Về ứng dụng có một số công cụ (AiT, StackAnalysis, TVLA) nhưng còn rất nhiều hạn chế, chỉ dừng lại ở mức hỗ thực nghiệm trong nghiên cứu, khi đưa vào ứng dụng trong thực tế chưa đáp ứng được các yêu cầu của ngành công nghiệp phần mềm. Astrée là công cụ thương mại thành công nhất hiện nay, tuy nhiên miền ứng dụng khá hẹp nên chưa được ứng dụng rộng rãi. Với tình hình nghiên cứu cơ bản và xu thế công nghệ phần mềm trên thế giới hiện nay tập trung vào các vấn đề lớn như quy mô và chất lượng của các sản phẩm phần mềm, kỹ thuật giải thích trừu tượng là một dải nghiên cứu và ứng dụng quan trọng đối với ngành công nghệ phần mềm. Việc tiến hành đề tài nghiên cứu trong lĩnh vực này là cần thiết trong việc nâng cao chất lượng nghiên cứu cơ bản ứng dụng vào thực tế kiểm soát chất lượng phần mềm. 1.4. Kết luận chương 1 Trong chương 1 luận văn đã trình bày tổng quan về phân tích chương trình, các ý tưởng chính cần thiết cho việc nghiên cứu kỹ thuật giải thích trừu tượng và vai trò của kỹ thuật này trong phân tích chương trình tĩnh. Khảo sát tình hình nghiên cứu ở trong và ngoài nước, các xu hướng đang được ứng dụng của kỹ thuật này trong việc nâng cao chất lượng phần mềm. Về cơ sở lý thuyết nền tảng của kỹ thuật này như: ngữ nghĩa chương trình, ngữ nghĩa vết, các phương thức trừu tượng, biểu diễn trừu tượng của các ngữ nghĩa, …, sẽ được nghiên cứu sâu trong chương 2. 16 Chương 2 - CỞ SỞ LÝ THUYẾT CỦA KỸ THUẬT GIẢI THÍCH TRỪU TƯỢNG 2.1. Khái niệm về kỹ thuật giải thích trừu tượng Kỹ thuật giải thích trừu tượng (Abstract interpretation): Là một kỹ thuật trong phân tích chương trình, kỹ thuật này giúp giải thích về ngữ nghĩa của một chương trình với những hàm đơn điệu trên các tập hợp đã được xếp thứ tự. Lý thuyết giải thích trừu tượng nghiên cứu về ngữ nghĩa của chương trình, phương pháp trừu tượng hóa ngữ nghĩa của chương trình, và tính đủ (sound) cũng như tính chính xác (precise) của phương pháp xấp xỉ để tạo ra ngữ nghĩa trừu tượng. Kỹ thuật giải thích trừu tượng được hiểu theo nghĩa trực giác là việc thực thi một phần của một chương trình để lấy thông tin về nó: sơ đồ luồng điều khiển, sơ đồ luồng dữ liệu, … [8]. + Hình thức hóa: Tất cả những gì đã được chuẩn tắc hóa và được chứng minh chặt chẽ bằng toán học. + Phi hình thức hóa: dựa kinh nghiệm, thử nghiệm, mà không thể chứng minh được bằng toán học. Ứng dụng của kỹ thuật giải thích trừu tượng: Phân tích trừu tượng được ứng dụng trong phân tích cú pháp, trình biên dịch, gỡ lỗi chương trình ... 2.2. Ứng dụng của kỹ thuật giải thích trừu tượng Kỹ thuật giải thích trừu tượng được ứng dụng rộng rãi và là một phần không thể thiếu trong lĩnh vực kiểm thử phần mềm. Kỹ thuật giải thích trừu tượng được dùng để chứng minh tính đầy đủ, tính chính xác, tính đúng đắn cục bộ, tính đúng đắn toàn cục của hệ thống. Một số ứng dụng của giải thích trừu tượng như [8]: + Phân tích cú pháp của dòng lệnh: phân tích thuộc tính và cú pháp của các dòng lệnh bằng việc giải thích trừu tượng các thuộc tính và cú pháp. 17 + Phân tích tĩnh chương trình: đây là lĩnh vực được ứng dụng nhiều nhất của giải thích trừu tượng. Phương pháp này phân tích mã nguồn của chương trình bằng cách trừu tượng hóa các thực thi của chương trình đó. Từ đó chứng minh tính đủ, tính đúng đắn, tính chính xác của chương trình. + Ẩn thông tin: trong các ngôn ngữ dựa trên các phần mềm bảo mật, các thông tin được ẩn đi để tránh sự theo dõi, phát hiện bằng cách sử dụng việc trừu tượng hóa các thông tin của chương trình đó. + Ngoài ra giải thích trừu tượng còn nhiều ứng dụng quan trọng khác trong các ngành công nghiệp như xe hơi, hàng không, vũ trụ, ... 2.3. Một số khái niệm cơ bản 2.3.1. Ngữ nghĩa cụ thể của chương trình Ngữ nghĩa cụ thể của một chương trình được hình thức hóa (là một mô hình toán học của) mô tả tất cả các hành vi (quĩ đạo các đường thực thi) có thể của chương trình thực hiện trong tất cả các môi trường phù hợp, các thực thi có thể của chương trình được thể hiện trong hình 2.1. Hình 2.1 Sơ đồ hành vi có thể của chương trình. Ngữ nghĩa cụ thể của chương trình là vô hạn (tức là có vô số các đường thực thi như hình trên) các đối tượng toán học, do đó không thể thực hiện các tính toán trên miền ngữ nghĩa cụ thể của một chương trình. Tất cả các câu hỏi 18
- Xem thêm -

Tài liệu liên quan