Introduction

  • 计算机安全的核心原则 = 维护所计算信息的保密性 + 维护所计算信息的完整性

    保密性 = 信息只开放给授权用户

    完整性 = 维护信息的准确性 + 一致性

  • 信息流跟踪（IFT）是一种模拟系统计算时信息传播方式的安全技术。

    特点：拥有一些 tag 来表示安全类别，且这些 tag 可以更新。

  • 本次调研主要介绍硬件 IFT 分类方法，用于调查、分类、比较不同的硬件 IFT 技术。

Information Flow

  • IFT 技术的工作原理 = 用安全类别标记存储对象，并在计算数据时跟踪这些标签

Storage Objects and Processes

  • 存储对象是信息的容器，进程描述了对这些对象执行的计算。存储对象和进程因安全策略和抽象级别而异。

  • image-20230104101318676

    附：上图为安全语言结构示例。

Security Classes and Flow Relations

  • 信息流策略定义了数据对象之间允许的关系。为此，IFT 将每个对象与一个安全类别相关联，即给对象一个安全标签或安全标记。
  • 在实际中，大多数策略使用image-20230104101707494 两元素网络，允许将保密性和完整性相关的安全属性建模为image-20230104101833762

Noninterference

  • Noninterference 通过将所有系统输入、输出和状态建模为 high 或 low 来创建信息流模型，指出 high 的任何变化不应该导致 low 的输出变化。一个主要的挑战是硬件中的对象数量通常比软件中的多得多。

  • image-20230104102613227

    附：上图是 explicit flow 的一个简单示例。

Types of Information Flow Relations

  • 虽然流关系提供了一种方式来指定与是否允许信息在对象之间传输相关的安全策略，但是它们没有严格定义确定是否存在信息流的方法。 信息可以通过许多不同的方式传播。 理解不同类型的信息流关系以及它们如何在硬件中表现出来，是精确测量所有信息流并进一步严格执行安全策略的重要的第一步。

  • image-20230104102742921

    附：上图是 implicit flow 的一个简单示例。

Covert and Side Channels

  • Covert Channel 是使用非预期来源的信息传输。

    Covert Channels = storage channel + timing channel

  • Side Channel 是通过非功能(通常是物理)特征(例如，执行时间、功耗、电磁辐射和声发射)的信息泄漏。

Operator Precision

Precision of IFT

  • IFT 技术的精度反映了它准确测量硬件设计中所有现有信息流的能力。精确的 IFT 技术将精确地模拟硬件设计的信息流行为，而不精确的技术可能指示不存在的信息流，即假阳性（false positives），或者错过实际的信息流，即假阴性（false negatives）。

Imprecise IFT

  • 虽然不精确的 IFT 技术可能会导致保守的验证结果，但它们通常可以快速分析潜在的信息流安全漏洞， 这对于识别在罕见情况下发生的安全违规非常有用。

Precise IFT

  • 精确 IFT 技术在确定流量关系时考虑了硬件组件的功能和输入值， 该标签传播策略可以被形式化为输入及其标签的函数。

  • image-20230104104019463

    附：上图表示 flow relation 和 class combining operation的示例，显示了考虑和不考虑数据值的class combining operation的差异。

    • （a）是与门；
    • （b）是不考虑数据值的 flow relation 和 class combining operation；
    • （c）是考虑数据值的 flow relation 和 class combining operation。

Precision and Complexity Tradeoffs

  • 精确度和复杂性是评估硬件 IFT 技术的两个相互矛盾的因素，需要在两者之间进行权衡。

  • image-20230104104755791

    附：上图为与门推导简化的硬件 IFT 逻辑，展现了一种有效的方法来推导不同版本的具有可变精度和复杂度的布尔门硬件IFT逻辑，通过逐渐忽略输入，来放松精确度。

Security Properties

  • 信息流属性被表示为对象上的 flow relations。 属性指定存储在硬件对象中的信息能否流向其他对象。

    IFT 属性是超属性（hyperproperties）的例子，因为它们表达了需要跨多个轨迹验证的预期行为。

  • 硬件 IFT 工具使用存储安全相关信息的标签来模拟信息在硬件中的移动。标签指示对象是可信的还是不可信的，机密的还是公开的，是否包含时间变化等等。属性定义标签的初始条件，以及标签在执行过程中是否可以更改。

Confidentiality

  • 保密性属性确保任何与敏感对象(标记为 high)相关的信息永远不会流向未分类的对象(标记为 low)。

  • image-20230104110053926

    附：表1的前四行显示了各种硬件设计(如加密内核和算术单元)的保密性属性示例。使用assume语句将敏感对象的标签设置为high，并将公共可见对象的标签设置为low。

Integrity

  • 完整性是保密性的双重含义，在这里我们用 high 标签标记不可信的硬件资源，并用 low 标签标记它们不会影响关键组件。
  • image-20230104110053926附：表1显示了为加密核心（crypto cores）、调试单元（debug units）、处理器（processors）和访问控制单元（ access control units)编写的四个完整性属性。

lsolation

  • isolation 也可以作为信息流安全属性来实施。isolation 声明在具有不同信任级别的两个组件之间不应该有信息交换，是一种双向属性。

Constant Time

  • 信息流模型可用于捕获硬件设计中运行时变化产生的时序侧信道。 常数时间属性通过测量计算时间来评估是否可以检索敏感信息。 为了精确地捕获定时流，信息流模型需要区分逻辑流和定时流。

  • image-20230104111258616

    附：表2总结了几种在验证不同硬件设计中的时序侧通道时所使用的特性。

Design Integrity

  • IFT 可用于检测某些类型的未记录的设计修改，这些修改会泄漏敏感信息或通过在设计中插入恶意信息通道来覆盖关键内存位置。

  • image-20230104112205281

    附：表3总结了 Trust-HUB中GLIFT检测信息泄露的特性。

现有的IFT技术

基于状态机的IFT语言

Caisson 和 Sapper 是增强了 IFT 能力的 HDL 语言，可以直接生成执行所需 IFT 属性的电路。这两种语言都使用状态机进行硬件设计，并可以防止产生非法流。

Caisson 通过静态类型检查来执行。这迫使他保守地执行复制以限制信息流。这会带来很大的硬件区域开销。但也显著地提高逻辑能力。

Sapper 添加了动态类型系统以减少逻辑复制的需求。它通过采用混合方法进行标签检查来改进 Caisson。它使用静态分析生成一组动态检查，这些检查被插入到硬件设计中，以实现动态跟踪。这样可以重用资源，从而降低区域开销。

Coq

Coq 是一个交互式定理证明器。它允许数学断言的表达式，机械性地检查这些假设的证明，帮助寻找形式化的证明，并从构建性的证明中输出一个关于它的形式化规范的被证明有效的程序。Coq 不是一个自动定理证明器，但是包括自动定理证明工具以及各种决策流程。

VeriCoq-IFT

VeriCoq-IFT 自动将设计从 HDL 语言转换为 Coq 形式语言，无需重新设计硬件。

SecVerilog

SecVerilog 使用表达型类型系统扩展了 Verilog 语言。其使用的是静态类型检查方法。SecVerilog 用户需要显式地为代码中的每个变量添加安全标签。它使用类型系统来确保支持指定的信息流策略。

SecChisel

ChiselFlow 是另一种类型强制 HDL，带有用于开发安全硬件架构的定时标签。它已被用于创建具有硬件级信息流控制的加密加速器，并正式验证这些实现的安全性。

IFT验证技术

IFT 验证技术可以以静态或是动态的方式运行。静态 IFT 技术在设计期间通过模拟、形式化方法、仿真等来检查设计是否符合所需的安全属性。验证完成后，IFT 模型将被删除。动态硬件 IFT 是一种运行时机制，它通过跟踪逻辑来增强原始硬件设计，监视信息流行为并防止有害的信息流。通常需要付出额外的代价，例如，额外的资源使用和性能开销。

模拟（simulation）

模拟是验证硬件设计行为的常用方法。硬件安全模拟在测试台输入电路设计，观察结果是否违反了安全策略。

形式化方法验证

形式化验证工具可以通过等价性检验、SAT 求解、定理证明或类型检验等方式，对信息流模型的安全属性进行形式化(或半形式化)验证。形式化方法的好处是，对于已证明的属性，硬件保证是安全的。验证结果在很大程度上依赖于指定的安全属性的质量和完整性。

仿真（emulation）

随着 IC 验证平台的发展，领先的 EDA 公司也开发了工具来验证 FPGA 仿真服务器上硬件设计的信息流安全属性。硬件仿真通常比软件仿真的验证性能好 10 倍。仿真是一种很有前途的方法，它利用底层硬件的信息流测量功能来执行安全协同验证并检测利用硬件安全漏洞的软件攻击。

RTLIFT

一种 RTLIFT 的实现步骤如下所示：设计流程跟踪库；增强跟踪逻辑的组合电路；用跟踪隐式流所需的逻辑增强条件语句。

流跟踪库

为了通过 RTL 代码跟踪信息流，每个操作都应该进行检测，以便它可以同时对操作数的布尔值和安全标签进行操作。对于每个操作 OP，即 Z = X OP Y 是 Verilog 中的有效语句，我们定义了一个模块 OP_IFT，它接收输入 X 和 Y 以及它们的安全标签 X_t 和 Y_t，并生成输出 Z 和它的安全标签 Z_t。这些模块被预定义，并作为一个称为“流跟踪库”的输入文件提供给 RTLIFT 软件。

显式流跟踪

流跟踪首先要对每个数据位进行扩展，即在给定的 Verilog 代码中连接寄存器，使用标签承载关于数据安全属性的信息。

隐式流跟踪

仅仅跟踪显式流可能会因为忽略隐式流的存在而错误地报告条件语句中不存在流。为了跟踪这些流程，对于每个赋值操作，我们都会获得一个影响语句执行的变量列表。在这个列表中，我们生成跟踪隐式流所需的逻辑。

引用文献：
Register Transfer Level Information Flow Tracking for Provably Secure Hardware Design. Armaiti Ardeshiricham, Wei Hu, Joshua Marxen and Ryan Kastner Dept. of Computer Science and Engineering, University of California, San Diego

Hardware Information Flow Tracking. WEI HU, Northwestern Polytechnical University ARMAITI ARDESHIRICHAM and RYAN KASTNER, University of California, San Diego