Họ giao thức IPsec là tập hợp tất cả các phương tiện kỹ thuật đảm bảo việc bảo vệ truyền dữ liệu trên tầng IP và được coi là một cơ sở hạ tầng an toàn. Các đặc tả của IPsec v2 bao gồm mô tả cấu trúc đảm bảo an toàn truyền dữ liệu trong mạng IP, như giao thức bảo vệ dữ liệu Authentication Header (AH) và Encapsulating Security Payload (ESP), giao thức thiết lập tự động đường truyền bảo vệ Internet Key Exchange (IKEv2), cũng như thuật toán mã hóa xác thực và thuật toán mật mã. Các dịch vụ an toàn gồm: kiểm tra tính truy cập, tính toàn vẹn, xác thực nguồn dữ liệu, phát hiện và loại bỏ các tin phát lại (thuộc loại tính toàn vẹn một phần chuỗi tin), tính nhạy cảm của dữ liệu và tính nhạy cảm hạn chế của dòng dữ liệu. Các dịch vụ này được cung cấp trên tầng mạng và đảm bảo tính trong suốt đối với tầng vận chuyển và các tầng trên đó.

Phương pháp xây dựng bộ công cụ đánh giá các tính năng an toàn khi thực thi giao thức IPSec sẽ được phân tích dưới đây.

Khái quát phương pháp

Bài toán kiểm thử đối với IPsec bao gồm xây dựng các tác động thử nghiệm và đánh giá tính đúng đắn của các kết quả quan sát được. Vấn đề đánh giá tính đầy đủ của độ phủ – phạm vi của các tác động thử nghiệm càng rộng thì càng nhận được tính bao quát đầy đủ các chức năng giao thức khi thử nghiệm.

Các yêu cầu trong chuẩn quốc tế là các tài liệu không hình thức, tức là chỉ được viết dưới dạng các trạng thái mong muốn của hệ thống bằng ngôn ngữ tự nhiên. Nhằm đưa ra được các bài thử cho giao thức thì cần phải chuyển chúng về dạng thuận lợi có thể giải quyết được bài toán đặt ra. Thực hiện được việc này cần sử dụng các đặc tả hình thức mà ở đó các yêu cầu được đưa ra dưới dạng các biểu thức logic và được biểu diễn trực tiếp dưới dạng các công thức toán học.

Kiểm tra các chức năng an toàn bao gồm hai phương pháp là hình thức hóa các chuẩn của giao thức và hình thức hóa nhiệm vụ của các bộ thử nghiệm:

- Phương pháp hình thức hóa các chuẩn của giao thức bao gồm: phân tích các đặc tả của giao thức, lấy ra các yêu cầu, xác định giao diện hình thức của giao thức, hình thức hóa các yêu cầu chức năng đối với việc thực thi giao thức, đưa ra các tiêu chí phủ và tạo hàm bổ các trạng thái.

- Phương pháp hình thức hóa các chuỗi thử nghiệm cấu thành từ việc xác định mục đích thử nghiệm, đưa ra các bước chuyển cho máy thử nghiệm tự động, đưa ra hàm xác định trạng thái của máy thử nghiệm tự động theo trạng thái mô hình đặc tả kết nối của giao thức, thiết kế thông tin thiết lập của máy tự động thử nghiệm và tạo các định dạng để biểu diễn các lựa chọn cũng như bao gồm việc đẩy các kịch bản vào thử nghiệm và phân tích các kết quả thử nghiệm.

Trong hai phương pháp trên thì phương pháp hình thức hóa các chuẩn giao thức là một trong những bước quan trọng nhất của quá trình xây dựng bộ thử nghiệm. Bước này tạo cơ sở cho toàn bộ bộ thử nghiệm. Quá trình xem xét ở đây đã được cụ thể hóa áp dụng cho giao thức IPsec.

Quá trình hình thức hóa các đặc tả giao thức IPsec

Tổng hợp các yêu cầu

Đặc tả của các giao thức an toàn thông thường được thể hiện trong các tài liệu tiếng Anh (RFC, các chuẩn ISO,...) với các phát biểu cú pháp và ngữ nghĩa không hình thức. Chỉ có một vài yêu cầu được nhấn mạnh bằng các từ như MUST, SHOULD, MAY.... Nhưng hầu hết các yêu cầu chức năng gần như không được nêu riêng trong các tài liệu đó. Vì vậy nhiệm vụ của bước đầu tiên là phải tạo ra được danh sách đầy đủ các yêu cầu đối với giao thức nghiên cứu và phân tích chúng. Quá trình tổng hợp các yêu cầu này được giải quyết thông qua việc giải quyết bốn nhiệm vụ chính như sau:

-  Xác định tập hợp các tài liệu về giao thức

Các tài liệu hướng dẫn IPsec  do IETF đề xuất và đặc tả của các giao thức Internet được đưa ra dưới dạng IETF RFC bằng ngôn ngữ tiếng Anh. Việc phân tích cấu trúc các tài liệu này phải bắt đầu bằng việc nghiên cứu tổng quan các giao thức Internet nhằm phát hiện sự ràng buộc giữa các giao thức và đưa ra các danh sách RFC làm bước đệm cho việc nghiên cứu chi tiết.

-  Định danh các yêu cầu chức năng

Để có thể đảm bảo việc đưa ra đầy đủ các yêu cầu có nghĩa là tạo các liên kết liền mạch từ các đặc tả hình thức tới các yêu cầu theo các tài liệu chuẩn, cần thiết phải đưa các yêu cầu như là các đối tượng với định danh duy nhất. Đối với việc kiểm tra IPsec để giải quyết vấn đề này cần tạo ra bản liệt kê mục lục các yêu cầu.

Bản liệt kê mục lục các yêu cầu là danh sách các yêu cầu được qui định bởi các tài liệu IPsec và các ngữ cảnh chung của vùng đối tượng nghiên cứu (sau đây gọi tắt là Danh sách các yêu cầu). Ở đây đối với mỗi một yêu cầu được lấy ra từ các tài liệu, Danh sách các yêu cầu sẽ liên kết tới vị trí tương ứng trong tài liệu đó. Thông thường thì một yêu cầu loại này tương ứng với một đoạn văn bản logic thể hiện một qui định đối với một phần tử chức năng hoặc một phần tử dữ liệu nào đó. Mỗi yêu cầu này được định danh duy nhất. Danh sách các yêu cầu cho phép đánh giá tính đầy đủ hình thức và tính tương ứng của quá trình thử nghiệm giữa các tài liệu chuẩn và đối tượng nghiên cứu.

-  Hệ thống hóa các yêu cầu

Hệ thống hóa các yêu cầu nhằm chia các yêu cầu ra các nhóm “giống nhau”. Vì mục đích chính là tạo ra đặc tả hình thức các yêu cầu (để có thể công thức hóa và mô hình hóa bằng các biểu thức toán học, từ đó lập trình hóa các bộ thử nghiệm để kiểm thử), nên hệ thống hóa để đưa ra các nhóm yêu cầu được hình thức hóa theo các điểm giống nhau theo cách sau:

+ Chia thành các yêu cầu trạng thái và yêu cầu toàn vẹn. Yêu cầu trạng thái là các yêu cầu đối với trạng thái thực hiện giao thức IPsec trong những điều kiện hay trong những hoàn cảnh nhất định. Còn yêu cầu toàn vẹn là các yêu cầu đối với các mối liên kết giữa các phần tử trạng thái của giao thức, giữa các trường các tin của giao thức... mà chúng phải được thực thi trong suốt quá trình thực hiện chức năng của hệ thống và trong hầu hết các trường hợp phát sinh khi thực hiện giao thức.

+ Chia theo các đối tượng của yêu cầu. Các yêu cầu đặc tả được đưa ra đối với trạng thái của các thành phần và các đối tượng khác nhau trong cấu trúc của IPsec. Yêu cầu mô tả trạng thái của một đối tượng được đưa vào một nhóm. Điều này sẽ tạo điều kiện dễ dàng hơn trong việc sử dụng danh sách các yêu cầu trong các quá trình tiếp theo.

+ Chia theo mức độ cần thiết. Tiêu chí này thể hiện rằng trong rất nhiều giao thức đưa ra các chức năng của giao thức mà bắt buộc phải được thể hiện trong các thực thi hoặc không bắt buộc hỗ trợ trong các thực thi đó. Đối với đặc tả của IPsec đưa ra ba mức thể hiện sự cần thiết là bắt buộc, khuyến cáo và không bắt buộc

+ Chia các yêu cầu theo cộng và trừ. Yêu cầu cộng sẽ là các yêu cầu khi thực thi sẽ hoàn thành những hành động nào đó, ví dụ như gửi tin nhắn vào mạng hoặc trả lại mã trả lời nào đó. Yêu cầu trừ là các yêu cầu cấm việc thực thi hoàn thành những hành động nhất định. Ví dụ, đặc tả cấu trúc IPsec CẤM việc không thực thi sử dụng đồng thời thuật toán mã hóa và thuật toán chữ ký số. Tiêu chí này quan trọng khi thực hiện hình thức hóa bởi vì yêu cầu cộng và trừ được hình thức hóa theo các cách khác nhau. Tiêu chí này sẽ chia các yêu cầu ra làm hai lớp.

Các loại yêu cầu kể trên sẽ được đưa vào bản mục lục liệt kê các yêu cầu. Trong phạm vi các loại riêng biệt có các yêu cầu sẽ thuộc một loại nhưng thông thường sẽ bắt gặp trường hợp một yêu cầu sẽ thuộc nhiều tiêu chí. Trong trường hợp này, bản liệt kê sẽ đưa vào tất cả các loại yêu cầu.

-  Phân loại các yêu cầu theo đối tượng yêu cầu: Dựa trên các tài liệu khoa học đã được nghiên cứu, cũng như tính hợp lý trong phân chia theo đối tượng, các yêu cầu sẽ được phân loại theo: liên quan đến mối liên lạc giữa các trường tin của giao thức; tính toàn vẹn của trạng thái giao thức; xử lý các tin vào; nội dung các tin ra; xử lý các chuỗi tin; tương tác với các giao thức tầng dưới; tương tác với các giao thức tầng trên; liên quan tới giao diện phần mềm việc thực hiện IPsec.

Hình thức hóa các yêu cầu đặc tả

Bước tiếp theo sau khi lấy ra được các yêu cầu chức năng là phải hình thức hóa các yêu cầu đó. Việc hình thức hóa yêu cầu đặc tả được thực hiện theo các bước sau:

- Xác định giao diện hình thức của giao thức: Việc xác định giao diện hình thức (interface) của IPsec cần phải giải quyết các nhiệm vụ sau: Biểu diễn mối tương tác việc thực thi IPsec ở dạng tập hợp các sự kiện vào và ra; Xác định tập hợp các sự kiện trong tồn tại đối với mỗi trạng thái thực thi IPsec; Xác định các dấu hiệu của các phần tử giao diện hình thức dựa trên tập hợp các sự kiện được đưa ra.
Khi đưa ra giao diện hình thức cần tính đến các hạn chế liên quan tới các sự kiện được kích hoạt song song,... Tập hợp các phần tử được lựa chọn của giao diện hình thức phải đầy đủ để xây dựng mô hình trạng thái của hệ thống một cách tương ứng.

-  Tập hợp các sự kiện vào và ra đối với các chức năng khác nhau của IPsec:­­ Thành phần của giao diện hình thức đối với giao thức bảo vệ dữ liệu AH (Authentication Header) và ESP  được xây dựng như sau. Đối với mỗi tin nhắn sẽ được chuyển từ bảng chữ cái của tin nhắn sang giao diện hình thức bằng cách đưa ra hai phần tử là Tiếp nhận tin (trong phần tử này được đặc tả là xử lý các gói tin vào) và Gửi tin (đặc tả bằng việc kiểm tra tính chính xác của các tin đi).

Giao th­­­ức IKEv2 nằm trên tầng ứng dụng của TCP/IP và sử dụng giao thức UDP để trao đổi thông tin. Đặc tả của IKEv2 là các thông tin của giao thức này được xử lý trên tầng vận chuyển bằng các giao thức IPSec. Ở đây IKEv2 cũng được xây dựng một cách tương tự bao gồm hai phần tư là nhận và gửi tin IKEv2.

-  Xác định loại đối với các phần tử thể hiện chức năng của giao diện chương trình: Việc này cần thiết bởi vì việc thử nghiệm thường được tiến hành từ xa. Đối với các chức năng của giao diện chương trình thì điều này có nghĩa là các đặc tả sẽ được thực thi không phải ở trên các nút đích (trên đó hoạt động hệ thống cần thử nghiệm) mà ở trên các nút thiết bị. Điều này có nghĩa là trên các nút thiết bị có thể cài đặt các hệ điều hành hoàn toàn khác so với trên nút đích, vì vậy không đảm bảo được rằng hệ thống các loại thực thi sẽ tồn tại trên nút thiết bị.

-  Xác định các loại để biểu diễn các tin nhắn của giao thức: Cần xác định loại cho các sự kiện vào và ra của các tin nhắn. Đối với mỗi sự kiện sẽ thành lập các lớp (class) khác nhau phù hợp với đối tượng đầu vào và đầu ra. Ví dụ như đối với sự kiện receive_PDU tiếp nhận các tin vào với một tham số và không có tham số trả lại. Còn đối với sự kiện sent_PDU không có tham số vào còn kết quả trả lại là tin đi ra.

-  Tạo các điều kiện trước và sau đối với giao diện hình thức của giao thức an toàn: Trong cả hai trường hợp trên đều cần phải chuyển các bản không hình thức ở ngôn ngữ tự nhiên sang định dạng tương ứng với ngôn ngữ hình thức.

-  Tạo trạng thái mô hình: Để có thể tạo ra đặc tả chung không phụ thuộc vào các cách thực thi IPSec cụ thể cần phải có trạng thái mô hình cấu thành từ các đối tượng có ý nghĩa đối với tất cả các thực thi. Các cấu trúc dữ liệu này được xây dựng trên cơ sở mô hình khái niệm của giao thức.

-  Hình thức hóa các mối liên lạc ngữ nghĩa trong các tin của giao thức: Các mối liên lạc ngữ nghĩa giữa các trường được ghi ở một dạng bất biến thể hiện thông qua các tin nhắn ra. Đối với các tin nhắn vào, sự bất biến không được ghi lại bởi vì đối với các giao thức Internet cho phép nhận các tin phá vỡ các yêu cầu định dạng tin nhắn. Đối với giao thức IPsec có mô tả các nguyên tắc xử lý sự phá vỡ các định dạng và phạm vi toàn vẹn trong các tin nhắn.

-  Hình thức hóa các yêu cầu phủ định: Các yêu cầu phủ định cấm việc thực thi trạng thái nhất định. Các yêu cầu phủ định được hình thức hóa ở dạng các phản ứng khác nhau, ví dụ như được thể hiện bằng các biểu thức logic: if (expr) {return false;}.

-  Hình thức hóa các yêu cầu đối với phản ứng đợi, đối với việc bắt buộc phản ứng, đối với phản ứng sự kiện vào, phản ứng với kết thúc thời gian: dùng các phương pháp cho phép kiểm tra tính đúng đắn của các phản ứng nhận được. Đây cũng chính là việc hình thức hóa các phản ứng, kết quả các phản ứng với các sự kiện vào ra để có thể biểu diễn chúng dưới dạng các biểu thức toán học logic phục vụ cho việc xây dựng bộ thử nghiệm. Mỗi dạng phản ứng được mô tả bằng các hàm với các tham số vào và ra tương ứng.

Hình thức hóa các yêu cầu đối với các chức năng không bắt buộc và chức năng bất định: các hàm không bắt buộc là các chức năng của giao thức mà có thể không cần sử dụng trong các thực thi, còn các chức năng bất định là các chức năng mà không phải tất cả các nhánh trạng thái của nó được xác định trong đặc tả. Đối với các chức năng không bắt buộc, thì đặc tả hình thức bao gồm các tham số xác định việc cho các yêu cầu vào thành phần đặc tả. Phụ thuộc vào giá trị của tham số biểu thức logic hình thức hóa yêu cầu sẽ bỏ qua hoặc tính toán việc sử dụng đặc tả hình thức. Còn việc hình thức hóa các chức năng bất định có thể chia ra làm hai nhóm biểu thị là “cấm” và “cho phép”. Trong nhóm “cấm” việc thực thi sẽ cấm một cách rõ ràng việc đưa các kích thích tương ứng với các nhánh không xác định và cấm việc sử dụng các phần tử không xác định trong các phản ứng. Đối với nhóm “cho phép” sẽ mang các tham số mà giá trị của nó tương ứng với các phương án khác nhau cho phép sự bất định.

Kết luận

Quá trình hình thức hóa các chuẩn của giao thức bao gồm: phân tích các đặc tả của giao thức, lấy ra các yêu cầu, xác định giao diện hình thức  cần thực hiện đầu tiên và quyết định việc xây dựng bộ thử nghiệm có đầy đủ và bao quát đầy đủ các chức năng an toàn của IPSec hay không. Công việc tiếp theo để tiến tới xây dựng hoàn chỉnh một bộ thử nghiệm là xem xét cách hình thức hóa các đặc tả của IPSec, trên cơ sở đó tiến hành xây dựng việc thử nghiệm cho IPSec bao gồm cả việc xây dựng mô hình thử nghiệm, kiến trúc của phương pháp thử và các bài thử nghiệm cụ thể