本頁只刊出中文翻譯與中文說明；英文原文請見下方原文連結。
原文連結
論文資訊
- 類型：已發表論文
- 日期：2022-09-02
摘要
本文描述並評估了 DIG，這是一種動態不變量生成器，可從觀察到的程序追蹤中推斷出不變量，重點關注數值變量和數組變量。對於數值不變量，DIG 支援在數值程式變數上定義的非線性等式和任意程度的不等式。對於數組不變量，DIG 會產生多維數組變數之間的巢狀關係。這些屬性對於目前的靜態和動態不變分析方法來說非常重要且具有挑戰性。 DIG 與現有動態方法之間的主要區別在於其生成技術，它直接從跡線推斷出不變量，而不是使用跡線來過濾預先定義的模板。為了產生準確的不變量，DIG 採用了數學和形式方法領域的思想和工具，包括方程式求解、多面體構造和定理證明；例如，DIG 使用幾何形狀來表示和推理多項式不變量。 27 種數學演算法和 AES 加密實現的實驗結果證明 DIG 在為這些程式產生不變量方面是有效的。