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.

翻译：自2006年正式发布以来，统一可扩展固件接口（UEFI）已成为连接计算机硬件与操作系统的行业标准，取代了传统的BIOS系统。UEFI对系统资源拥有比包括系统内核在内的任何其他软件组件更高的特权安全访问权限。因此，识别并表征UEFI中的漏洞对计算机安全至关重要。然而，UEFI漏洞的自动化检测与表征仍面临严峻挑战：静态漏洞分析技术虽具备可扩展性，但缺乏精确性（会产生大量误报）；而符号分析技术虽然精确，却受限于路径爆炸和约束求解的计算开销导致的可扩展性问题。本文提出一种名为静态分析引导符号执行（STASE）的技术，该技术通过整合两种分析方法以发挥各自优势并弥补其不足。我们首先在LLVM字节码上执行基于规则的静态漏洞分析，以识别适合进行符号执行的潜在漏洞目标；随后针对每个目标集中进行符号执行，实现精确的漏洞检测与特征生成。STASE依赖于可复用漏洞规则与攻击者可控输入的手动定义，但自动化生成了引导符号执行过程的测试框架，从而解决了符号执行通常需要手动生成测试框架以缩减状态空间所面临的可用性与可扩展性难题。我们在UEFI代码库实现中应用了STASE，该技术成功检测并生成了近期报告的9个PixieFail漏洞中5个漏洞的特征，同时在Tianocore的EDKII代码库中发现了13个新漏洞。