Khái niệm chính:

• Watermark phần mềm: nhúng chữ ký (signature) vào chương trình để xác nhận quyền sở hữu.
• - Trình tấn công: được mô hình hóa như trình phân tích trừu tượng (abstract interpreter).
• - Signature được nhúng dưới dạng thuộc tính ngữ nghĩa Mt(s), chỉ có thể trích xuất nếu phân tích hoàn chỉnh với Mt(s).

Khung watermark ngữ nghĩa:

• Stegomarker Mt: ánh xạ chữ ký s → chương trình chứa watermark.
• - Stegoembedder £: kết hợp chương trình gốc P với watermark Mt(s) → chương trình đã đóng dấu Ps.
• - Stegoextractor β: phân tích Ps để trích xuất s nếu β hoàn chỉnh với Mt(s).

Định nghĩa hệ watermark:

• Một hệ watermark là bộ ba (S, Mt, β) sao cho Ps = £(P, Mt(s)) có ngữ nghĩa giống Mt(s) với đầu vào kích hoạt (enabling input), và giống P với đầu vào khác.
• - Việc trích xuất watermark là bài toán hoàn chỉnh (completeness) trong phân tích trừu tượng.

Đặc tính đánh giá watermark:

▪ Độ bền (Resilience):

  - Tấn công biến đổi chương trình (distortive attack) là phép biến đổi t giữ nguyên ngữ nghĩa.

  - Hệ watermark bền với t nếu t không phá vỡ thuộc tính Mt(s).

  - Phân loại: t-resilient, t-vulnerable, t-ineffective.

▪ Độ bí mật (Secrecy):

  - Hệ watermark bí mật nếu attacker không thể phân biệt các chương trình chứa các chữ ký khác nhau.

  - Mô hình hóa bằng non-interference trừu tượng bậc cao (HOANI).

  - Định nghĩa attacker mạnh nhất mà vẫn không phá vỡ bí mật.

▪ Độ minh bạch (Transparence):

  - Hệ watermark minh bạch nếu attacker không phân biệt được chương trình gốc và chương trình đã đóng dấu.

  - Định nghĩa attacker mạnh nhất mà vẫn không phát hiện watermark.

▪ Độ chính xác (Accuracy):

  - Hệ watermark chính xác nếu chương trình gốc và chương trình đã đóng dấu có hành vi giống nhau với người dùng.

  - Mô hình hóa bằng ngữ nghĩa denotational và ánh xạ quan sát ao.

Kiểm chứng mô hình:

▪ Kỹ thuật watermark động (path-based):

  - Nhúng chữ ký bằng chuỗi lựa chọn tại các điều kiện (true/false) khi chạy chương trình với đầu vào đặc biệt.

  - Watermark là chuỗi nhị phân của chữ ký.

  - Không bền với tấn công biến đổi luồng điều khiển.

▪ Kỹ thuật watermark tĩnh (graph-based):

  - Nhúng chữ ký bằng đồ thị vào CFG của chương trình.

  - Đánh dấu các khối mã để dễ trích xuất.

  - Không bền với tấn công làm phẳng CFG.

Kết luận:

• Khung lý thuyết ngữ nghĩa cho phép mô hình hóa watermark phần mềm một cách chính xác và tổng quát.
• - Các kỹ thuật watermark hiện tại đều là trường hợp đặc biệt của watermark ngữ nghĩa.
• - Việc trích xuất watermark là bài toán hoàn chỉnh trong phân tích trừu tượng.
• - Khung này giúp đánh giá và so sánh các kỹ thuật watermark theo tiêu chí lý thuyết.