sysss-blogs

摘要： Introduction 現有的靜態分析工具都是 unsound 的，并且體現為 uniformly unsound。這里的“uniformly”指靜態分析工具會用一種統一地忽略所有不能處理的特性，而不考慮代碼上下文。這種策略會減少誤報率 \(\frac{false \ alarm}{all \ a 閱讀全文

摘要： Introduction Context-sensitivity 會帶來靜態分析的精度提升，但是也會帶來巨大的開銷，這引出一個關鍵的問題：能否在某些對整體分析的精度有重要影響的函數上選擇性的使用 context-sensitivity？這個問題的難點在于識別具有這種性質的函數。文章總結了在 cont 閱讀全文

摘要： 主要關注 Tool Integration and Retrieval Enhancement 這一部分。 將外部工具與 LLM 集成是單一代理突破自身生成能力邊界的關鍵之一，代表工作包括： ToolCoder：Arxiv'23 LLM 在特定上下文下會生成錯誤的 API 調用，ToolCoder通 閱讀全文

摘要： Survey 站在 security 研究者的角度來關注 LLM + 程序分析的如下幾個方向： 靜態分析：在不同的下游應用上評估 LLM 的作用，下游應用包括 vulnerability detection，malware detection，program verification, static 閱讀全文

摘要： 一個 context-insensitive 的 Andersen 風格的分析算法： 定義： \(N\) 是變量和 new 的總數量 \(D(x)\) 是解引用變量 \(x\) 的 statements 數量 \(G\) 是 flow graph \(E\) 是 flow graph 到達不動點時邊 閱讀全文

摘要： Subtyping 提到的規則并不適合實現，原因在于 T-SUB 和 S-Trans 規則推導中的項 \(t\) 沒有任何約束的元變量（沒有對形狀作出限制）。 這意味著對于任意一個項 \(t\)，無法確定在什么時機使用什么規則做類型推導。 S-Trans 的另一個問題是，\(U\) 的搜索空間近乎無 閱讀全文

摘要： （因為最近在搓類型系統，發現 tapl 也就學了個皮毛，再回來補充一下知識） Subtyping 關系滿足：自反性，傳遞性 對于 record 類型有寬度和深度兩個規則： 寬度對應的子類型關系有點難以理解，具備更多的 field 的 record 反而是“更小”的子類型。但是從類型對應的值集來看，更 閱讀全文

摘要： Background 在構建一個自頂向下的語法分析器時，很多情況下需要處理復雜的模式匹配來完成解析。比如對于文法： E ::= '[' A ']' | '(' B ')' 需要寫出如下 OCaml 代碼： let parseE input = match input with | '[' :: re 閱讀全文

摘要： ![](https://img2 閱讀全文

摘要： Introduction 之前的一些 JS 的 callgraph 相關的工作忽略了動態屬性訪問（比如 Field-based Analysis）。最近的 ECOOP'22 的工作顯示動態屬性訪問是最主要的 unsoundness 的來源。這篇文章主要關注動態屬性訪問，使用 dynamic pre- 閱讀全文