Luận văn công nghệ chương trình kèm chứng minh - Máy ảo VEP và EPCC

Luận văn nghiên cứu công nghệ chương trình kèm chứng minh PCC, EPCC, phân tích kỹ thuật xác minh bảo mật máy ảo VEP và ứng dụng thực tế.

• Người hướng dẫn: Danny Dubé
• Trường học: Université Laval
• Chuyên ngành: An toàn thông tin
• Đề tài: Công nghệ chương trình kèm chứng minh PCC và EPCC
• Loại tài liệu: khóa luận
• Năm xuất bản: 2009
• Địa điểm: Laval

Tóm tắt

I. Khám Phá Công Nghệ Chương Trình Kèm Chứng Minh PCC Nền Tảng An Toàn Phần Mềm Hiện Đại

Trong kỷ nguyên số, an toàn phần mềm là yếu tố then chốt. Công nghệ chương trình kèm chứng minh (Proof Carrying Code - PCC), ra đời năm 1996 bởi George Necula và Peter Lee, cung cấp một giải pháp đột phá. PCC cho phép người tiêu dùng xác minh tính bảo mật của chương trình không đáng tin cậy thông qua các bằng chứng do nhà sản xuất cung cấp. Quá trình xác minh bảo mật chương trình này diễn ra chỉ một lần khi khởi chạy, giúp duy trì hiệu suất ứng dụng. Sự đơn giản và linh hoạt trong triển khai khiến PCC trở thành một nền tảng vững chắc cho việc xây dựng các hệ thống an toàn phần mềm thế hệ mới. Mục tiêu chính là giảm thiểu sự tin cậy cần thiết vào bên thứ ba, đặt quyền kiểm soát an ninh vào tay người dùng cuối.

1.1. PCC là gì Định nghĩa và tầm quan trọng trong bảo mật ứng dụng

Proof Carrying Code (PCC) là một cơ chế cho phép người tiêu dùng mã nhận được một chương trình cùng với một bằng chứng toán học chứng minh rằng chương trình đó tuân thủ một chính sách bảo mật cụ thể. Bằng chứng này được kiểm tra bởi một trình kiểm tra tin cậy nhỏ gọn trên máy của người dùng. Tầm quan trọng của PCC nằm ở khả năng cung cấp sự đảm bảo an toàn cho các chương trình không đáng tin cậy trong các môi trường phân tán hoặc từ xa. Nó cho phép người dùng chủ động xác minh hành vi của mã trước khi thực thi, giảm thiểu rủi ro bảo mật mà không ảnh hưởng đến hiệu suất sau lần kiểm tra đầu tiên. Công nghệ chương trình kèm chứng minh PCC tạo ra một lớp bảo vệ vững chắc chống lại các mối đe dọa tiềm ẩn.

1.2. Lợi ích vượt trội và những hạn chế của Proof Carrying Code

PCC mang lại nhiều lợi ích vượt trội. Đầu tiên, nó bảo toàn hiệu suất chương trình vì quá trình xác minh chỉ thực hiện một lần. Thứ hai, PCC đơn giản và linh hoạt trong triển khai, dễ dàng tích hợp vào nhiều hệ thống. Nó cho phép người tiêu dùng tự kiểm tra tính tuân thủ chính sách bảo mật của mã, tăng cường đáng kể độ tin cậy của an toàn phần mềm. Tuy nhiên, PCC cũng có những hạn chế. Kích thước bằng chứng có thể lớn, tạo gánh nặng lưu trữ và truyền tải. Việc tạo bằng chứng đòi hỏi tài nguyên tính toán lớn từ nhà sản xuất. Mặc dù các biến thể như OPCC và PPCC đã giải quyết một phần, việc áp dụng rộng rãi công nghệ chương trình kèm chứng minh PCC vẫn cần cải tiến, dẫn đến sự phát triển của các khung làm việc như EPCC nhằm tối ưu hóa các nhược điểm này.

II. Phân Tích Các Kỹ Thuật PCC Từ Truyền Thống Đến Các Phương Pháp Tối Ưu

Sự phát triển của công nghệ chương trình kèm chứng minh PCC không ngừng cải tiến để giải quyết các thách thức ban đầu. Từ mô hình PCC truyền thống đến các biến thể nâng cao như OPCC, PPCC và FPCC, mỗi kỹ thuật đều mang lại những đóng góp quan trọng. Việc phân tích sâu sắc các phương pháp này giúp hiểu rõ hơn về cách chúng tối ưu hóa hiệu quả và giảm bớt gánh nặng trong quá trình xác minh bảo mật chương trình. Các cải tiến tập trung vào việc giảm kích thước bằng chứng, đơn giản hóa quá trình kiểm tra, và tăng cường tính linh hoạt cho việc triển khai PCC. Nắm vững các kỹ thuật này là chìa khóa để áp dụng thành công công nghệ chương trình kèm chứng minh PCC và EPCC trong thực tiễn.

2.1. Tìm hiểu kiến trúc và giao thức của hệ thống PCC truyền thống

Kiến trúc của PCC truyền thống bao gồm một nhà sản xuất mã (code producer) và một người tiêu dùng mã (code consumer). Nhà sản xuất tạo ra mã thực thi cùng với một bằng chứng chứng minh mã đó tuân thủ một chính sách bảo mật cụ thể. Bằng chứng này sau đó được gửi đến người tiêu dùng. Tại phía người tiêu dùng, một trình kiểm tra bằng chứng đáng tin cậy (proof checker) sẽ nhận bằng chứng và mã, sau đó xác minh tính hợp lệ của bằng chứng đối với mã. Giao thức của PCC truyền thống thường tuân theo các bước: mã được biên dịch, bằng chứng được tạo, bằng chứng và mã được gửi đi, sau đó bằng chứng được kiểm tra. Nếu bằng chứng hợp lệ, mã sẽ được thực thi. Quá trình này đảm bảo rằng mọi chương trình không đáng tin cậy đều phải trải qua bước kiểm tra nghiêm ngặt trước khi được phép chạy, nâng cao an toàn phần mềm. Mặc dù hiệu quả, kiến trúc này đôi khi tạo ra bằng chứng có kích thước lớn, dẫn đến nhu cầu cải tiến.

2.2. Các cải tiến đáng kể OPCC PPCC FPCC giải quyết thách thức

Để khắc phục những hạn chế của PCC truyền thống, nhiều kỹ thuật cải tiến đã được phát triển. OPCC (Optimized Proof Carrying Code) tập trung vào việc giảm kích thước của bằng chứng, làm cho quá trình truyền tải và lưu trữ hiệu quả hơn. Mục tiêu là duy trì khả năng kiểm chứng mà vẫn giảm thiểu tài nguyên. PPCC (Practical Proof Carrying Code) của Andrew W. Appel và cộng sự giảm thiểu cơ sở tính toán đáng tin cậy (Trusted Computing Base - TCB), làm cho hệ thống trở nên mạnh mẽ hơn trước các lỗi hoặc lỗ hổng trong các thành phần tin cậy. FPCC (Foundational Proof Carrying Code) hướng đến việc xây dựng các bằng chứng dựa trên các nguyên tắc cơ bản hơn, tăng cường độ tin cậy toán học của quá trình xác minh. Các cải tiến này chứng tỏ sự nỗ lực liên tục trong việc làm cho công nghệ chương trình kèm chứng minh PCC trở nên thiết thực và dễ áp dụng hơn trong các tình huống thực tế, mở đường cho sự ra đời của EPCC như một khung làm việc toàn diện hơn.

III. Công Nghệ EPCC Khung Chứng Minh Mở Rộng Cho An Toàn Chương Trình Nâng Cao

EPCC (Extended framework for Proof Carrying Code) là một bước tiến quan trọng trong lĩnh vực công nghệ chương trình kèm chứng minh PCC. Khung làm việc này được đề xuất bởi Danny Dubé và Heidar Pirsadeh Tabari từ Đại học Laval, nhằm giải quyết các thách thức chưa được giải quyết triệt để bởi các kỹ thuật PCC trước đó. EPCC giới thiệu một kiến trúc mạnh mẽ, tập trung vào việc cải thiện khả năng mở rộng, tính linh hoạt và đặc biệt là việc xác minh bảo mật chương trình một cách tự động. Trung tâm của kiến trúc EPCC là một máy ảo chuyên dụng được gọi là VEP (Virtual Machine for EPCC), đóng vai trò then chốt trong quá trình kiểm chứng an toàn. Khám phá công nghệ chương trình kèm chứng minh PCC và EPCC giúp người dùng hiểu rõ hơn về tiềm năng của nó.

3.1. Kiến trúc EPCC và vai trò trung tâm của máy ảo VEP

Kiến trúc EPCC được thiết kế để cung cấp một nền tảng vững chắc cho việc chứng minh tính an toàn của các chương trình không đáng tin cậy. Nó bao gồm các thành phần chính như công cụ tạo bằng chứng, trình kiểm tra bằng chứng, và đặc biệt là máy ảo VEP. Máy ảo VEP được coi là trái tim của EPCC, nơi mã được thực thi sau khi đã được xác minh. VEP không chỉ là một môi trường thực thi mà còn là một thành phần quan trọng trong việc đảm bảo an toàn phần mềm. Các đặc tính của VEP, như quản lý bộ nhớ và tập lệnh, được thiết kế đặc biệt để hỗ trợ quá trình kiểm chứng bảo mật. VEP cung cấp một môi trường được kiểm soát chặt chẽ, nơi các bằng chứng có thể được áp dụng và xác minh hiệu quả, từ đó đảm bảo rằng mã chỉ thực hiện các hành động tuân thủ chính sách bảo mật đã định. Sự tích hợp chặt chẽ của VEP vào khung EPCC cho phép một quy trình xác minh bảo mật chương trình hiệu quả và đáng tin cậy.

3.2. Những đóng góp chính của EPCC trong việc tăng cường kiểm chứng mã

EPCC mang lại nhiều đóng góp chính trong việc tăng cường kiểm chứng mã. Một trong số đó là việc cung cấp một khung làm việc mở rộng, có khả năng thích ứng với nhiều loại chính sách bảo mật và ngôn ngữ lập trình khác nhau. Điều này giúp EPCC linh hoạt hơn so với các kỹ thuật PCC truyền thống. Hơn nữa, EPCC tập trung vào việc tự động hóa quá trình chứng minh bảo mật cho máy ảo VEP, một khía cạnh quan trọng để giảm thiểu sự can thiệp thủ công và nâng cao hiệu quả. Các đề xuất trong luận án này nhằm mục đích làm cho quá trình chứng minh bảo mật của VEP trở nên tự động hơn, giảm thiểu lỗi và tăng tốc độ xác minh. Bằng cách tích hợp chặt chẽ việc kiểm chứng vào môi trường thực thi (thông qua VEP), EPCC cung cấp một giải pháp toàn diện cho việc đảm bảo an toàn phần mềm và xử lý chương trình không đáng tin cậy một cách hiệu quả.

IV. Bí Quyết Kiểm Chứng Bảo Mật Máy Ảo VEP của EPCC Đảm Bảo An Toàn Tuyệt Đối

Máy ảo VEP là một thành phần cốt lõi của công nghệ EPCC, và việc đảm bảo an toàn phần mềm cho nó là tối quan trọng. Quá trình kiểm chứng bảo mật máy ảo VEP đòi hỏi sự kết hợp giữa các phương pháp xác minh thủ công và tự động. Mục tiêu là chứng minh rằng VEP tuân thủ các quy tắc an toàn đã định, ngay cả khi thực thi chương trình không đáng tin cậy. Sự chính xác trong quá trình kiểm chứng trực tiếp ảnh hưởng đến độ tin cậy của toàn bộ hệ thống EPCC. Một quy trình kiểm chứng chặt chẽ giúp phát hiện sớm các lỗ hổng tiềm ẩn, từ đó củng cố khả năng phòng thủ của công nghệ chương trình kèm chứng minh PCC và EPCC trước các mối đe dọa an ninh mạng.

4.1. Quy trình xác minh thủ công Ưu điểm và giới hạn

Trong quá khứ, việc xác minh bảo mật các hệ thống phức tạp như máy ảo VEP thường được thực hiện thủ công. Quy trình này bao gồm việc phân tích mã nguồn, kiểm tra từng dòng lệnh và logic chương trình bằng mắt thường, hoặc sử dụng các công cụ phân tích tĩnh đơn giản. Ưu điểm của xác minh thủ công là khả năng phát hiện các lỗi logic tinh vi hoặc các vấn đề bảo mật không rõ ràng mà các công cụ tự động có thể bỏ sót. Nó đòi hỏi kiến thức chuyên sâu và sự tỉ mỉ từ các chuyên gia bảo mật. Tuy nhiên, phương pháp này có những giới hạn đáng kể: nó tốn thời gian, dễ mắc lỗi do con người, và không thể mở rộng đối với các chương trình lớn hoặc phức tạp. Với sự phát triển của công nghệ chương trình kèm chứng minh PCC, nhu cầu về các phương pháp kiểm chứng nhanh chóng và đáng tin cậy hơn trở nên cấp thiết, thúc đẩy sự phát triển của các công cụ xác minh tự động.

4.2. Phương pháp kiểm tra tự động Hiệu quả và độ tin cậy

Để vượt qua các giới hạn của xác minh thủ công, các phương pháp kiểm tra tự động đã được phát triển để tăng cường hiệu quả và độ tin cậy trong việc xác minh bảo mật máy ảo VEP. Các kỹ thuật này bao gồm sử dụng các công cụ chứng minh định lý, phân tích hình thức (formal analysis), và các trình kiểm tra mô hình (model checking). Những công cụ này có khả năng tự động phân tích hành vi của VEP và chứng minh rằng nó tuân thủ các chính sách bảo mật đã định. Chẳng hạn, việc sử dụng các công cụ như Frama-C cho phép phân tích mã C của VEP để tìm kiếm các lỗi an ninh hoặc chứng minh các thuộc tính an toàn. Kiểm tra tự động không chỉ giúp tiết kiệm thời gian và tài nguyên mà còn giảm thiểu khả năng mắc lỗi do con người. Điều này là đặc biệt quan trọng trong việc đảm bảo an toàn phần mềm cho các hệ thống phức tạp như EPCC, nơi sự chính xác tuyệt đối là cần thiết để xử lý chương trình không đáng tin cậy một cách an toàn.

V. Nguyên Tắc Đảm Bảo An Toàn Cho Chương Trình Không Đáng Tin Cậy Góc Nhìn Chuyên Gia

Để xây dựng một hệ thống an toàn phần mềm mạnh mẽ, việc hiểu rõ các nguyên tắc đảm bảo an toàn cho chương trình không đáng tin cậy là vô cùng quan trọng. Các nguyên tắc này định hình cách chúng ta tiếp cận việc xác minh bảo mật chương trình và giảm thiểu rủi ro. Chúng bao gồm các phương pháp phân tích cả trước và trong quá trình thực thi, cũng như việc tối thiểu hóa các thành phần hệ thống cần được tin cậy. Khi áp dụng công nghệ chương trình kèm chứng minh PCC và EPCC, việc tuân thủ các nguyên tắc này giúp tối đa hóa hiệu quả bảo mật và xây dựng lòng tin cho người tiêu dùng mã. Một hệ thống an toàn phải có khả năng kiểm soát chặt chẽ hành vi của mã, ngăn chặn mọi vi phạm chính sách bảo mật đã thiết lập.

5.1. Phân tích tĩnh và động Các phương pháp bảo mật trước và trong thực thi

Để đảm bảo an toàn phần mềm cho chương trình không đáng tin cậy, có hai phương pháp phân tích chính: phân tích tĩnh và phân tích động. Phân tích tĩnh được thực hiện trước khi chương trình chạy, bằng cách kiểm tra mã nguồn hoặc mã bytecode để tìm kiếm các lỗ hổng bảo mật hoặc chứng minh các thuộc tính an toàn. Các kỹ thuật như kiểm tra mô hình (model checking), phân tích luồng dữ liệu, và diễn giải trừu tượng (abstract interpretation) thuộc nhóm này. Phân tích tĩnh giúp phát hiện lỗi sớm mà không cần thực thi chương trình. Ngược lại, phân tích động diễn ra trong quá trình chương trình đang chạy. Một 'màn hình thời gian chạy' (runtime monitor) sẽ quan sát hành vi của chương trình và có thể dừng nó nếu phát hiện nguy cơ vi phạm chính sách bảo mật. Cả hai phương pháp đều có vai trò riêng, bổ trợ cho nhau để cung cấp một lớp bảo vệ toàn diện, là nền tảng của công nghệ chương trình kèm chứng minh PCC.

5.2. Tối thiểu hóa hạ tầng đáng tin cậy TCB Chìa khóa cho hệ thống an toàn

Một nguyên tắc cơ bản trong việc thiết kế hệ thống an toàn phần mềm là tối thiểu hóa hạ tầng đáng tin cậy (Trusted Computing Base - TCB). TCB là tập hợp các phần cứng, phần mềm cơ bản (firmware), và phần mềm mà hệ thống phải tin cậy tuyệt đối để đảm bảo an ninh. Nếu có lỗi hoặc lỗ hổng bên trong TCB, toàn bộ an ninh của hệ thống có thể bị xâm phạm. Do đó, việc thu nhỏ TCB càng nhiều càng tốt sẽ làm giảm bề mặt tấn công và tăng cường độ tin cậy tổng thể. Với công nghệ chương trình kèm chứng minh PCC, người tiêu dùng có thể xác minh tính an toàn của mã mà không cần tin cậy toàn bộ môi trường phát triển của nhà sản xuất. Điều này giúp chuyển gánh nặng kiểm chứng sang người tiêu dùng với một TCB nhỏ gọn (chủ yếu là trình kiểm tra bằng chứng). Nguyên tắc này là trọng tâm của PCC và các khung làm việc như EPCC, đảm bảo rằng chỉ những thành phần thực sự cần thiết mới được tin cậy hoàn toàn, tăng cường đáng kể an toàn phần mềm cho các chương trình không đáng tin cậy.

VI. Tương Lai của Công Nghệ Chương Trình Kèm Chứng Minh Hướng Phát Triển và Triển Vọng

Công nghệ chương trình kèm chứng minh PCC và EPCC đang mở ra những hướng phát triển đầy hứa hẹn trong lĩnh vực an toàn phần mềm. Để giải quyết các thách thức còn tồn đọng và nâng cao khả năng áp dụng thực tiễn, các nghiên cứu tập trung vào việc tối ưu hóa quy trình chứng minh, tích hợp các công cụ mạnh mẽ, và tự động hóa việc xác minh. Sự phát triển này không chỉ củng cố vị thế của PCC như một giải pháp bảo mật hiệu quả mà còn mở rộng phạm vi ứng dụng của nó. Tương lai của công nghệ chương trình kèm chứng minh nằm ở khả năng cung cấp các giải pháp xác minh bảo mật chương trình linh hoạt, hiệu quả và đáng tin cậy cho mọi loại chương trình không đáng tin cậy trong môi trường ngày càng phức tạp.

6.1. Vai trò của công cụ chứng minh định lý và Frama C trong kiểm chứng

Trong việc phát triển công nghệ chương trình kèm chứng minh PCC và EPCC, các công cụ chứng minh định lý đóng một vai trò quan trọng. Chúng cho phép các nhà nghiên cứu và nhà phát triển chứng minh một cách hình thức (formally prove) các thuộc tính an toàn của mã. Frama-C là một ví dụ điển hình về công cụ như vậy. Đây là một nền tảng phân tích và xác minh mã nguồn C, cho phép người dùng chú thích mã với các đặc tả hình thức và sau đó sử dụng các plugin để kiểm tra các thuộc tính đó. Trong bối cảnh EPCC và máy ảo VEP, Frama-C có thể được sử dụng để xác minh tính đúng đắn và an toàn của mã nguồn VEP, đảm bảo rằng các thành phần cốt lõi hoạt động như mong đợi và không chứa lỗ hổng. Việc tích hợp các công cụ mạnh mẽ này giúp tăng cường đáng kể độ tin cậy của quá trình xác minh bảo mật chương trình, giảm thiểu rủi ro khi xử lý chương trình không đáng tin cậy và củng cố an toàn phần mềm.

6.2. Các đề xuất cho việc chứng minh tự động bảo mật heap trong VEP

Một trong những lĩnh vực nghiên cứu quan trọng trong tương lai của EPCC là việc chứng minh tự động bảo mật heap trong VEP. Bộ nhớ heap là nơi thường xuyên xảy ra các lỗi bảo mật như tràn bộ đệm (buffer overflows) hoặc sử dụng bộ nhớ sau khi giải phóng (use-after-free), có thể dẫn đến các lỗ hổng nghiêm trọng. Việc phát triển các phương pháp và công cụ để tự động chứng minh rằng máy ảo VEP quản lý bộ nhớ heap một cách an toàn là một thách thức lớn nhưng cần thiết. Các đề xuất trong lĩnh vực này thường liên quan đến việc sử dụng logic hình thức, hệ thống kiểu nâng cao (advanced type systems), hoặc các kỹ thuật phân tích con trỏ để đảm bảo rằng mọi hoạt động trên heap đều tuân thủ chính sách bảo mật của VEP. Thành công trong việc tự động hóa chứng minh bảo mật heap sẽ củng cố đáng kể khả năng của công nghệ chương trình kèm chứng minh PCC và EPCC trong việc cung cấp an toàn phần mềm toàn diện và đáng tin cậy cho các chương trình không đáng tin cậy, mở rộng phạm vi ứng dụng trong các hệ thống phức tạp.

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

Remerciements Je Gens 4 remereicr vivement Monsicur Danny Dubé, professcur de Université Laval, de m’avoir accueilli au sein de son équipe de recherche, de m’avoir toujours encouragé, de m’avoir donné des suggestions précieuses dans Ia recherche. Je Iui en suis trés reconnaissant. Je ens 4 remercier également les professeurs cL les personnels de l'Institut de la Francophonie pour Informatique, des professeurs invités de m’avoi donné des cours de haut qualité et pour leur soutien tout au long de mes études. Je voudrais remercicr mes amis dans mun laboratoire de recherche, Bui Nguyen Minh, Haythem Kefi, Joseph Assouramou, Marieme Doua, Ishagh Mayouf de m’avoir donnée leurs conscils, curs commentaires cl leurs souliens pendant Ie temps J effectuais ma recherche.

Yadresse un grande merci 4 ma famille pour leur soutien et leur encouragement de toute F instance Table des matiéres List des figures Résumé Abstract. Contexte du stage Problématique kỳ Trimeipes đ”assuror la sócurilẻ pour le consommatcur ue wo 4 Contributions 5. Harry Chapitre I RR Techniques principales de PCC. Technique PCC traditionnel.1 Architecture du systéme PCC traditionnel 1.2 Protocole de PCC traditionnel.

Implémentation du technique PCC traditionnel.4 Contributions du technique PCC traditionnel 10 Technique OPCC 12 tà 2.1 Architecture du systeme OPCC.2 Contribution du technique OPCC 13 Technique FPCC 13 3.1 Architecture du systéme FPCC 13 3.2 Implémentation de technique FPCC. Contribution de technique FPCC 15 Technique EPCC 16 4.1 Architecture du technique EPCC 16 4.2 Contribution de technique EPCC AT Chapitre TT 18 Verification de la sécurité du machine virtuelle d’EPCC. Présentation de la machine virtuelle VEP 1B 11 Bnévement 18 1.2 Gestion de mémoire 19 1.3 Ensemble des instructions de VEP.4 Assurance la sécurité de VEP 24 Verification de la sécurilé de la VEP = 2.1 Vẻrification manuelle de la VEP.2 Vénfication automatique de la VEP. 2B Chapitre IV 34 Conclusion et perspecties.

Oulil pourle prouveur de théorème 37 2. Utilisation de Frama-C. ¬— 38 3 Spécification de sécurité du tas dans la VEP 39 Réferences 42 ait Abstract Introduced for the first time in November 1996 by George Necula and Peter Lee “I from university Camegie Melon, proof carrying code (PCC) is a promising method ‘for verifying the security of an untrusted program executed on a cade consumer by using proofs generated by code producer. The verification is performed only for the first run of the program so the performance of program is not affected This technique is also attractive for the simplicity and flexibility in the deployment process.

However, there are still some disadvantages that make it difficult to apply the model widely in reality. Some of them are solved in the research of Andrew W. Appel et al (PPCC "!, reducing the trusted computing based), of George Necula (OPCC ÏŸ, reducing the size of proof). this thesis aims to carry out a research on major techniques of proof carnring cade, to analyse the advantages and disudvantage of each technique.

An important part in this thesis concentrates on the framework EPCC (Extended framework for Proof Carrying Code) proposed by Danny Dubé and Heidar Pirsadeh Tabari from University Laval, the architecture of the virtual machine for EPCC (VEP ©), the heart of EPCC as well as some propositions for proving automatically its security. Résumé La technologie dex programmes accompagnés de preuves (Proof Carrying Code, PCC) a été introduite pour la premiere fois en Novembre 1996 dans le projet de recherche de George Necula et Peter Lee“ de Vuniver Carnegie Melon. Cette méthode est pour but de vérifier la sécurité d’un programme inéprouvé sur le consommateur de code en utilisant des preuves générées par le producteur de codes. Car la vérification enire les codes et les preuves est effectuée une seule fois dés le premier démarrage du programme, sa performance est donc préservée.

La méthode est connu aussi par sa simplifié, sa flexibilité dans le déploiement. Pourtant il existe encore des points faibles qui empéche Vapplication de PCC en réalité, en basant sur les points de vue différents, les chercheurs ont domme leur facon d’améliorer le modéle primitif comme limiter la taille de Vinfrasiructure présumée fiable (dens le modéle EPCC ©, Andrew W. Appel), réduire (a taille des preuves (dans le modéle OPCC™, Necula) Ce mémoire vise @ réaliser ume recherche sur les techniques principales de programmes accompagnés de preuves, a analyser ses avantages et aussi ses incunvénients. On se concentrera sur la méthode programmes accompagnés de preuves étendu (EPCC /) propesé par Danny Dubé et Lleidar Pirzadeh labari de PUniversité Laval.

On discutera également Uarchitecture d’une machine virtuelle (PEP !"'), le coeur du EPCC, et proposer un prototype pour prouver automatiquement la sécurité de celle machine. dự Résumé La technologie dex programmes accompagnés de preuves (Proof Carrying Code, PCC) a été introduite pour la premiere fois en Novembre 1996 dans le projet de recherche de George Necula et Peter Lee“ de Vuniver Carnegie Melon. Cette méthode est pour but de vérifier la sécurité d’un programme inéprouvé sur le consommateur de code en utilisant des preuves générées par le producteur de codes. Car la vérification enire les codes et les preuves est effectuée une seule fois dés le premier démarrage du programme, sa performance est donc préservée.

La méthode est connu aussi par sa simplifié, sa flexibilité dans le déploiement. Pourtant il existe encore des points faibles qui empéche Vapplication de PCC en réalité, en basant sur les points de vue différents, les chercheurs ont domme leur facon d’améliorer le modéle primitif comme limiter la taille de Vinfrasiructure présumée fiable (dens le modéle EPCC ©, Andrew W. Appel), réduire (a taille des preuves (dans le modéle OPCC™, Necula) Ce mémoire vise @ réaliser ume recherche sur les techniques principales de programmes accompagnés de preuves, a analyser ses avantages et aussi ses incunvénients. On se concentrera sur la méthode programmes accompagnés de preuves étendu (EPCC /) propesé par Danny Dubé et Lleidar Pirzadeh labari de PUniversité Laval.

On discutera également Uarchitecture d’une machine virtuelle (PEP !"'), le coeur du EPCC, et proposer un prototype pour prouver automatiquement la sécurité de celle machine. dự Résumé La technologie dex programmes accompagnés de preuves (Proof Carrying Code, PCC) a été introduite pour la premiere fois en Novembre 1996 dans le projet de recherche de George Necula et Peter Lee“ de Vuniver Carnegie Melon. Cette méthode est pour but de vérifier la sécurité d’un programme inéprouvé sur le consommateur de code en utilisant des preuves générées par le producteur de codes. Car la vérification enire les codes et les preuves est effectuée une seule fois dés le premier démarrage du programme, sa performance est donc préservée.

La méthode est connu aussi par sa simplifié, sa flexibilité dans le déploiement. Pourtant il existe encore des points faibles qui empéche Vapplication de PCC en réalité, en basant sur les points de vue différents, les chercheurs ont domme leur facon d’améliorer le modéle primitif comme limiter la taille de Vinfrasiructure présumée fiable (dens le modéle EPCC ©, Andrew W. Appel), réduire (a taille des preuves (dans le modéle OPCC™, Necula) Ce mémoire vise @ réaliser ume recherche sur les techniques principales de programmes accompagnés de preuves, a analyser ses avantages et aussi ses incunvénients. On se concentrera sur la méthode programmes accompagnés de preuves étendu (EPCC /) propesé par Danny Dubé et Lleidar Pirzadeh labari de PUniversité Laval.

On discutera également Uarchitecture d’une machine virtuelle (PEP !"'), le coeur du EPCC, et proposer un prototype pour prouver automatiquement la sécurité de celle machine. dự Chapitre I - Intruduction logiciel ne sont pas exceptions. En effet, le correctif le plus récent de Microsoft (8- Sep-2009) corrige 31 failles de sécurité dans lcsquellcs Š failles sont classées dans la catégorie des failles critiques. Dans l’attente du prochain correctif, comment le client pourrait-il se protéger contre des attaques? Tl faudrait par cons¢quent disposer d'un moyen simple, mais assez forge pour contrer les actions qui violent les politiques de sécurité au niveau du client.

Avec aide de technique programme accompagné des preuves (Proof Carrying Code, PCC) le consommateur peut verifier est ce que le logiciel fournit par Je producteur est conforme & sa politique de sécurité ou non. D’ailleurs, application de PCC ne diminue pas Ja performance de programme et la consommation de ressources (mémoire, processeur) de PCC sur le consommateur est limitée au maximum En basant sur les principes d’assurer la sécurité, on analysera les points forts, points faibles de chaque technique PCC et leurs applications en réalité et foumnit un prototype pour vénfier la sécurité de la machine virtuelle. Principes d’assurer la sécurité pour le consommateur Pour le consommaiteur, en général, on est capable de contrdler la sécurité d'un logiciel avant ou pendant son exécution. Pour assurer la sécurité avant l'exécution, on effectue une analyse statique sur le code en utilisant un outll qui décompose le programme sans Ì'oxéouter eL analyse tous les comportements possibles pour prouver que le programme soit sécurité.

Les implementations en réalité de ce type d’assurance sont Ie « Model checking» 21, analyser flux de donnée ŠÌ, interprétation abstraite I1 Pendant l’exécution, on a l’analyse dynamique, ou on fait marcher le programme et utilise un « runtime monitor » pour observer, et l'arréter si dans I’étape suivante, le programme causera une viclation. Toules les mesures de sécurité sur le client suivenl un principe de base: minimiser linfrastucture présumée fiable (‘rusted Computing Based, ‘(CB "4, Je (CB đun systéme est l'ensemble des matériaux, des microprogrammes et des logiciels qui se font confiance entre eux et auxquels fe client fait confiance, s’il existe des bugs a Tintérieur du TCB, Ja sécurité du systéme pourrait dre compromise. Par contre, les autres composants en dehors du ‘CK ne pourront jamais toucher sa sécurité Chapitre II Techniques principales de PCC 1. Technique PCC traditionnel 1.1 Architecture du systéme PCC traditionnel De point de vue de fonctionnalité, on a deux acteurs dans un systéme PC producteur de code et le consommateur de code.

Le consommutour de ceds su compose de deux composanis principaux : un géndrateur de condition de vérification (VCGen) et un examinateur de preuves. I] définit ses politiques de sécurité. Le VCGen s’occupe de représenter la combmaison de ces politiques et le résultat d’analyser statique du programme sous forme d’mne condition de verification (VC). C'est une formule logique qui reprdsenic Ie respect de là politique par le code en cours de vérification.

Si la formule est vraie alors le code est sécurilaire. L’autre composant, ’examinaicur de preuves réulise unc tesle sur ses politiques de sécurité avec les preuves fourntt par le producteur de code. 3i la preuve garantit que la VC ost vraie et dunc que le code est sécuritaire, le code [ournit par le producteur est autorisé d’exécuter sur le consommateur. Ty a deux composanis 4 cété de producteur de code : le compilateur certifié pour compiler le code source au format cxéculable avec des annotations (pré-condition, post-condition, invariant de la boucle, .) et le prouveur de théoréme pour générer des preuves qui ont accompagnés avec le programme.

Le consommateur de code doit effectuer des opérations sécuritaires et done qu'il ne peut pas sơ permetize d'excouter du code qui pourrait étre dangereux. I] exige donc que le producteur du code joigne une preuve de sécurité au code qu'il fournit. Dans la figure 1, le TCB du systéme contient tous les composants du consommateur (les objels non-gris), Les composants ct les données de producteur de code ne sont pas dans le TCB du consommateur, ils sont les composants qui n'ont pas 4 étre sévurilaires, Une caravlérisique originale du PCC est que Von {ait conliance au consommateur du code en utilisant des preuves méfiantes générées par le producteur de code qui est aussi méfiant Résumé La technologie dex programmes accompagnés de preuves (Proof Carrying Code, PCC) a été introduite pour la premiere fois en Novembre 1996 dans le projet de recherche de George Necula et Peter Lee“ de Vuniver Carnegie Melon. Cette méthode est pour but de vérifier la sécurité d’un programme inéprouvé sur le consommateur de code en utilisant des preuves générées par le producteur de codes.