用于表征故障脆弱性的攻击者模型推断

该博士项目致力于解决嵌入式系统上的注入式攻击问题，其研究重点从针对固定攻击者模型验证漏洞情况，转向构建能够描述攻击者能力与系统防御机制的模型。该研究涉及将归纳推理应用于二进制符号执行技术，以对攻击者模型进行形式化处理及扩展。

职位说明： 项目描述： 嵌入式系统容易受到故障注入攻击，攻击者通过物理干扰硬件来改变程序执行过程并引发安全漏洞。目前，代码抗攻击性的自动验证依赖于预定义的攻击者模型（关于攻击者能力的一系列假设，如故障数量、故障位置等）。 主要问题在于，该模型被预先作为假设而选取。如果模型存在轻微不准确之处，分析结果便无法通用应用。此外，现有工具通常仅提供单个攻击示例（即证据），无法全面揭示使系统处于脆弱状态的特定攻击者能力。 论文研究目标 本研究的目标是颠覆当前的研究范式：不再仅验证某段代码是否易受特定攻击者模型的攻击，而是旨在综合并分析使代码既易受攻击又具有抗性的各种攻击者模型。 研究目标是从对故障脆弱性的描述转向对攻击者的描述，具体通过识别以下要素实现： 能够成功执行攻击的最小攻击者模型。 用于确保代码受到保护的最大攻击者模型。 科学研究方法 本研究将利用归纳推理技术（推断原因与前提条件），并将其应用于二进制级别的符号执行分析。核心思路在于扩展此前用于分析脆弱程序输入时的归纳技术，并将其适用于攻击能力的构建。 主要科学挑战包括： 形式化：制定关于攻击者模型的相关标准，并建立它们之间的关联关系（例如，攻击者格子）。 推理语言：设计适用于生成攻击模型的语法和输入语言（例如，对比特翻转、注入限制、位置及频率的约束）。 可扩展性：优化位向量与阵列理论算法，以确保该方法能够适用于实际的大型代码库。 方法与预期影响 博士研究生将把其研究成果整合到 BINSEC 中，该工具属于 CEA 列表中的二进制符号执行引擎。实验将在真实的基准测试及受保护代码上进行（例如：Wookey 引导加载程序、Sentry 微内核、FISSC 基准测试）。 潜在影响十分显著： 评估：为认证实验室（CESTIs）与安全评估员提供关键支持。 行业：安全组件设计人员的申请（例如：苹果公司、ARM、ST、泰尔系统）。 安全性：有望扩展至非目标故障的分析领域（例如空间应用中的宇宙辐射）。

所需个人背景与技能要求： 计算机科学或应用数学领域的硕士学位或工程学位。核心技能： 扎实的数学逻辑与形式化方法基础（静态分析、验证）。 编程能力要求（优先选择 OCaml 或 C/C++）。 对网络安全与二进制代码分析具有浓厚兴趣。所需素质：科学严谨性、强大的抽象能力及独立意识