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漏洞的自动化检测与表征仍是一个具有挑战性的难题。静态漏洞分析技术虽具备可扩展性，但精度不足（易产生大量误报）；而符号分析技术虽精度较高，却因路径爆炸和约束求解的计算开销而面临可扩展性瓶颈。本文提出一种名为静态分析引导的符号执行技术，该技术融合了两种分析方法，以发挥各自优势并弥补其不足。我们首先在LLVM位码上执行基于规则的静态漏洞分析，以识别适合进行符号执行的潜在漏洞目标；随后针对每个目标集中进行符号执行，实现精确的漏洞检测与特征生成。STASE依赖于可复用漏洞规则与攻击者可控输入的手动定义，但实现了引导符号执行过程的测试框架自动化生成——这解决了符号执行通常需手动构建测试框架以缩减状态空间所导致的可用性与可扩展性问题。我们在UEFI代码库实现中应用了STASE，该技术成功检测并生成了9个近期披露的PixieFail漏洞中5个漏洞的特征，同时在Tianocore的EDKII代码库中发现了13个新漏洞。