Since its major release in 2006, the Unified Extensible Firmware Interface (UEFI) has become the industry standard for interfacing a computer's hardware and operating system, replacing BIOS. UEFI has higher privileged security access to system resources than any other software component, including the system kernel. Hence, identifying and characterizing vulnerabilities in UEFI is extremely important for computer security. However, automated detection and characterization of UEFI vulnerabilities is a challenging problem. Static vulnerability analysis techniques are scalable but lack precision (reporting many false positives), whereas symbolic analysis techniques are precise but are hampered by scalability issues due to path explosion and the cost of constraint solving. In this paper, we introduce a technique called STatic Analysis guided Symbolic Execution (STASE), which integrates both analysis approaches to leverage their strengths and minimize their weaknesses. We begin with a rule-based static vulnerability analysis on LLVM bitcode to identify potential vulnerability targets for symbolic execution. We then focus symbolic execution on each target to achieve precise vulnerability detection and signature generation. STASE relies on the manual specification of reusable vulnerability rules and attacker-controlled inputs. However, it automates the generation of harnesses that guide the symbolic execution process, addressing the usability and scalability of symbolic execution, which typically requires manual harness generation to reduce the state space. We implemented and applied STASE to the implementations of UEFI code base. STASE detects and generates vulnerability signatures for 5 out of 9 recently reported PixieFail vulnerabilities and 13 new vulnerabilities in Tianocore's EDKII codebase.
Cache timing attacks allow third-party observers to retrieve sensitive information from program executions. But, is it possible to automatically check the vulnerability of a program against cache timing attacks and then, automatically shield program executions against these attacks? For a given program, a cache configuration and an attack model, our CACHEFIX framework either verifies the cache side-channel freedom of the program or synthesizes a series of patches to ensure cache side-channel freedom during program execution. At the core of our framework is a novel symbolic verification techniq…
In this paper, we present a concolic execution technique for detecting SQL injection vulnerabilities in Android apps, with a new tool we called ConsiDroid. We extend the source code of apps with mocking technique, such that the execution of original source code is not affected. The extended source code can be treated as Java applications and may be executed by SPF with concolic execution. We automatically produce a DummyMain class out of static analysis such that the essential functions are called sequentially and, the events leading to vulnerable functions are triggered. We extend SPF with ta…
Smart contracts are executable programs that enable the building of a programmable trust mechanism between multiple entities without the need of a trusted third-party. Researchers have developed several security scanners in the past couple of years. However, many of these analyzers either do not scale well, or if they do, produce many false positives. This issue is exacerbated when bugs are triggered only after a series of interactions with the functions of the contract-under-test. A depth-n vulnerability, refers to a vulnerability that requires invoking a specific sequence of n functions to t…
The security development lifecycle (SDL) is becoming an industry standard. Dynamic symbolic execution (DSE) has enormous amount of applications in computer security (fuzzing, vulnerability discovery, reverse-engineering, etc.). We propose several performance and accuracy improvements for dynamic symbolic execution. Skipping non-symbolic instructions allows to build a path predicate 1.2--3.5 times faster. Symbolic engine simplifies formulas during symbolic execution. Path predicate slicing eliminates irrelevant conjuncts from solver queries. We handle each jump table (switch statement) as multi…
Android Framework is a layer of software that exists in every Android system managing resources of all Android apps. A vulnerability in Android Framework can lead to severe hacks, such as destroying user data and leaking private information. With tens of millions of Android devices unpatched due to Android fragmentation, vulnerabilities in Android Framework certainly attract attackers to exploit them. So far, enormous manual effort is needed to craft such exploits. To our knowledge, no research has been done on automatic generation of exploits that take advantage of Android Framework vulnerabi…
Smart contract, one of the most successful applications of blockchain, is taking the world by storm, playing an essential role in the blockchain ecosystem. However, frequent smart contract security incidents not only result in tremendous economic losses but also destroy the blockchain-based credit system. The security and reliability of smart contracts thus gain extensive attention from researchers worldwide. In this survey, we first summarize the common types and typical cases of smart contract vulnerabilities from three levels, i.e., Solidity code layer, EVM execution layer, and Block depend…
Zhejiang Gongshang University（浙江工商大学）；Zhejiang University（浙江大学）；National University of Singapore（新加坡国立大学）；Southern University of Science and Technology（南方科技大学）；Zhejiang Lab（之江实验室）
Smart contract vulnerability detection draws extensive attention in recent years due to the substantial losses caused by hacker attacks. Existing efforts for contract security analysis heavily rely on rigid rules defined by experts, which are labor-intensive and non-scalable. More importantly, expert-defined rules tend to be error-prone and suffer the inherent risk of being cheated by crafty attackers. Recent researches focus on the symbolic execution and formal analysis of smart contracts for vulnerability detection, yet to achieve a precise and scalable solution. Although several methods hav…
NetTantra Technologies (India) Pvt. Ltd.（NetTantra技术（印度）私人有限公司）；Virtual and Augmented Reality Centre of Excellence, IIT Bhubaneswar（布巴内斯瓦尔印度理工学院虚拟与增强现实卓越中心）；School of Minerals, Metallurgical and Materials Engineering, IIT Bhubaneswar（布巴内斯瓦尔印度理工学院矿物、冶金与材料工程学院）；Centre of Excellence for Novel Energy Materials, IIT Bhubaneswar（布巴内斯瓦尔印度理工学院新型能源材料卓越中心）
Vulnerability detection and safety of smart contracts are of paramount importance because of their immutable nature. Symbolic tools like OYENTE and MAIAN are typically used for vulnerability prediction in smart contracts. As these tools are computationally expensive, they are typically used to detect vulnerabilities until some predefined invocation depth. These tools require more search time as the invocation depth increases. Since the number of smart contracts is increasing exponentially, it is difficult to analyze the contracts using these traditional tools. Recently a machine learning techn…
