打算早上先看一個視頻，具體瞭解一下抽象解釋的相關概念，下午把 Tracer: Signature-based Static Analysis for Detecting Recurring Vulnerabilities 看了

SIG-程序分析 技术沙龙 数值程序分析—陈立前（国防科技大学）

不變式（值）生成

抽象解釋：對程序語義進行抽象（近似）的通用理論

Galois 連接

抽象域

image-20231014095701310

數值抽象域，在其上的析取，合取

image-20231014095821500

多面躰域（綫性不等式域），八邊形域（刻畫+1,-1,0，兩個變量之間的關係）

上近似：無漏報但是可能存在誤報

凸抽象域（綫性抽象域），凸抽象域（區間綫性抽象域，絕對值綫性抽象域）

數值程式分析

  • 結合抽象域與SMT的程式分析
  • 軟件中資源使用量上界分析
  • 神經網絡架構中的數值缺陷檢測

他人提問:

  • 應該選擇什麽樣的抽象域
  • 怎麽去自動化地檢測抽象域的精度
  • …