Static Analysis of String Encoders and Decoders
Static Analysis of String Encoders and Decoders
复制标题
DOI：
10.1007/978-3-642-35873-9_14
复制
发表时间：
2013-01
期刊：
影响因子：
--
通讯作者：
Loris D'antoni;Margus Veanes
中科院分区：
文献类型：
--
作者：
Loris D'antoni;Margus Veanes
人们对操纵字符串的程序的静态分析一直很感兴趣，特别是在网络安全的背景下。许多类型的安全漏洞都是通过程序中的缺陷暴露出来的，例如字符串编码器、解码器和消毒器。最近的工作集中在结合自动机和可满足性模理论技术来解决这些程序中的安全问题。这些技术可扩展到更大的字母表，如Unicode，这是Web软件中使用的事实上的字符编码标准。一种方法是使用字符谓词来泛化有限状态换能器。这项技术使得对一大类典型的消毒例程进行精确分析成为可能。然而，它一直无法很好地应对解码器，后者通常需要一次阅读一个以上的字符。为了克服这一局限性，我们引入了一种符号有限换能器(SFT)的保守推广，称为扩展符号有限换能器(ESFTS)，它结合了有界先行的概念。在我们的评估中，我们使用了UTF-16到UTF-8的翻译器(utf8编码器)和UTF-8到UTF-16的翻译器(utf8解码器)。在其他性质中，我们证明了utf8编码器和utf8解码器在功能上是正确的。
There has been significant interest in static analysis of programs that manipulate strings, in particular in the context of web security. Many types of security vulnerabilities are exposed through flaws in programs such as string encoders, decoders, and sanitizers. Recent work has focused on combining automata and satisfiability modulo theories techniques to address security issues in those programs. These techniques scale to larger alphabets such as Unicode, that is a de facto character encoding standard used in web software.One approach has been to use character predicates to generalize finite state transducers. This technique has made it possible to perform precise analysis of a large class of typical sanitization routines. However, it has not been able to cope well with decoders, that often require to read more than one character at a time. In order to overcome this limitation we introduce a conservative generalization of Symbolic Finite Transducers (SFTs) called Extended Symbolic Finite Transducers (ESFTs) that incorporates the notion of a bounded lookahead. We demonstrate the advantage ESFTs on analyzing programs for which previous approaches did not scale.In our evaluation we use a UTF-16 to UTF-8 translator (utf8encoder) and a UTF-8 to UTF-16 translator (utf8decoder). We show, among other properties, thatutf8encoderandutf8decoderare functionally correct.