安全微控制器设计中的逐步正式开发流程

可在www.sciencedirect.com在线获取理论计算机科学电子笔记280（2011）3-22www.elsevier.com/locate/entcsB语言在安全微控制器设计中的应用Marc Benveniste马克·本弗尼斯特1，2，3安全微控制器部门STMicroelectronics法国鲁塞的摘要安全关键软件的逐步正式开发现在是一个完善的工程实践，在铁路系统中很明显。然而，它并没有成功地应用于硬件开发，其中形式化方法主要用于验证和门级转换和优化。在本文中，我们报告了我们最近的经验，逐步正式发展的一个真正的宏细胞，开辟了道路，同步数字电路的设计与零功能缺陷。我们提出了一个开发流程，适合于获得证明正确的建设电路，进一步拥有额外的鲁棒性安全芯片所需的。所报告的工作是前瞻性的，旨在展示这种技术用于高置信度可信设备的可行性。关键词：形式化开发流程、数位电路、强健性、安全微控制器、建构修正。1引言这项工作的第一个贡献表明了逐步将正式的安全策略模型转换为实现它的安全功能的可合成硬件描述的可行性这项工作的第二个贡献，提高了实验正式开发流程，使鲁棒性也可以在一个行之有效的方式处理这项工作的第三个贡献是一个实验性的结合抽象解释和模型检查，以验证一组给定的属性的算法之前，任何尝试实现它。最后，我们报告了已确定的未解决问题，这些问题需要进一步的研究和开发工作。1个由Provenc e-Alpes-Conted' A zur（PAC A）R e g i ona l C o n c i l ST M -f o c u e d Forcoment支持的部件项目，PS-17 bis，与Clearsy系统工程密切和富有成效的合作2 部分由Medea+2A 303Biop@ss项目支持。3电子邮件：marc. st.com1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.11.0144M. Benveniste/电子笔记在理论计算机科学280（2011）32迈向正式发展进程数字电路的传统开发流程在很大程度上依赖于在铸造厂启动制造过程之前执行的验证步骤的测试。下图1显示了典型微控制器功能开发的第一步中Fig. 1. 微控制器电路编写测试程序，运行和分析模拟，代表了这第一个开发任务的一个重要部分。验证计划完全基于专业设计师的专业知识和经验。验证活动的覆盖率是通过使用一些专门的工具来衡量的，但功能规范的覆盖率充其量主要是同行评审的问题：唯一可用的参考是对要设计的功能的自然语言描述。一 个 简 单 的 想 法 是 我 们 工 作 的 基 础 。 考 虑 一 个 安 全 关 键 软 件 开 发 -ParisM′etroLine14atomatedsystem [25]，可以注意到，通过使用支持B技术的逐步改进方法[2]，在整个开发过程中进行了验证。简单的想法是将这种B形式化方法应用于我们的数字电路的开发。事实上，微电子开发工具已经采用了许多正式的方法，但它们主要是在幕后使用的，即设计师没有意识到它们的存在，更重要的是，它们的应用程序只有在源代码编写完成后才开始这些方法用于验证目的，并用于从寄存器传输级（RTL）表示到最终放置和路由网表的长路径中的各种转换。然而，更昂贵的功能错误通常在第一行代码编写之前就已经引入了。它们通常来自功能性的、高层次的设计，或者M. Benveniste/电子笔记在理论计算机科学280（2011）35甚至详细的设计规范。如前所述，这些自然语言表示没有可用的验证工具只有彻底的同行评审才有可能在这些错误种子开花之前过滤掉这些错误行为，一旦嵌入电路。我们定义并体验了一个用例[4]，一个新的开发流程，它广泛使用了形式证明，并在其功能行为和接口定义方面产生了一个经过彻底验证的源代码（见图2）。这个源代码，实际上是VHDL，可以直接合成。因此，它有能力进入标准工业流程的其余部分。该实验开发流程依赖于事件B [1]中表达的所需功能的正式模型，事件B是B方法针对系统开发的最新发展。我们相信，这种新的流程可以用于以一种经过验证的正确的方式构建任何数字功能。Analog功能不在这些技术的范围内，但它们的数字接口被用作正式的正确性合同，以便将它们包含在经过验证的数字电路中。图二、根据案例研究的定义和经验，3个结果建议的流程从一个巨大的抽象步骤开始。设计器必须编写一个只有几行的Event-B模型，以捕获要设计的函数的基本实现这一目标绝非易事。即使是训练有素的工程师也需要进行多次试验请记住，简单几乎总是很难实现的。6M. Benveniste/电子笔记在理论计算机科学280（2011）3我们经历的案例研究也不例外。我们不得不挣扎了一段时间才说出以下几点：定义3.1[基本属性]存储器保护单元的基本属性是监视微处理器执行的所有访问。此功能是要在安全微控制器上实施的访问控制安全策略的核心，如图3所示。图3.第三章。 案例研究：安全微控制器的存储器保护单元初步物业水平模型以简化方式呈列于图4。随着嵌入到主机微控制器中，逐步介绍了所设计功能的实现细节。改进计划的主要策略是逐步定义和转换表示访问权限矩阵r0的变量。双重变换一方面通过引入不同类型的访问及其相关细节来引导，另一方面通过权限矩阵的实现表示来引导。应该注意的是，我们的改进路径受到已经实现所需功能的遗留模块的限制。 这就是为什么接口规范和数据表第一章中的数据被确定为图2中开发流程的输入：前者为模块和总线协议提供线级接口;后者定义寄存器地址、名称、功能、位含义和程序员指南。图5提供了嵌入在通用微控制器公共数据手册[23]中的定时器描述示例。尝试了各种改进路径和策略，通常会导致死胡同或复杂的情况，证明工作将变得势不可挡。的M. Benveniste/电子笔记在理论计算机科学280（2011）37系统MPU集AD;CL;BY;TY抽象常数C 0，R 0性能C 0∈CL sR 0变量c0，r0，v0不变c0∈ CLsr0初始化工具c0，r0，v0：=C 0，R 0，事件allow=ANYa0，d0，t0哪里a0∈ AD s< $d0∈ BYs <$t0∈TYsn（a0<$→c0<$→d0<$→t0）∈r0然后v0：=0|| c0：∈CL s|| r0 : ∈ ADs × CLs × BYs ↔ TYs结束语：deny=ANYa0，d0，t0哪里a0∈ AD s< $d0∈ BYs <$t0∈TYsn（a0<$→c0<$→d0<$→t0）/∈r0然后v0：=真结束端见图4。案例研究：初始属性级别模型我们最终建立的细化计划有两个重要的“不”属性：没有覆盖范围的损失和没有不确定性。事实上，由于这个时钟电路必须在每个周期对任何输入组合都有明确的行为，因此Event-B模型必须实现一个总的确定性函数：• 它的事件的警卫的分离必须是真空真实的。此外，我们规定在细化事件时不得引入“漏洞”。当一个（抽象的）事件ea被（具体的）事件eci定义（分裂）时，如果析取具体事件的守卫是由抽象事件的守卫所隐含的可以肯定的是，没有无论何时，无论何时，（抽象）事件eai被（具体）事件ec所细化（分组），我们必须证明具体事件我们称这种性质为覆盖性质;• 非确定性行为被禁止用于安全微控制器。我们必须确保事件是两两互斥的。我们称这种性质为排他性性质。通过在Event-B系统工程工具Atelier B中生成额外的证明义务来实施这些属性[3]。请注意，在每个细化阶段证明这些属性减少了证明义务的总数，特别是对于排他性属性，本质上是组合的。为了对我们提出的开发数字电路的策略进行详细说明，以下段落概述了主要的改进阶段。8M. Benveniste/电子笔记在理论计算机科学280（2011）3图五、案例研究：数据手册级描述示例，此处为定时器寄存器3.1第一水平第一个改进引入了不同类型的访问，如数据的读（TyR）和写（TyW），代码的取（TyX），开始中断（TyB）和结束中断（TyE），以及无访问（TyN）。后者最初被遗忘，但被保险范围证明义务所强调。这些事件都是根“积极”事件允许的细化 存取矩阵r0更精确地定义为矩阵的集合，每个矩阵对应一种存取类型。这些矩阵中的每一个在这个阶段都是未定义的。只有它们与r0的关系被完全定义，如图6所示。下一个改进介绍了在中断和主机微控制器复位条件下驱动一些异常的自动机。只有自动机的状态和相关事件执行的转换被保存在下一个细化中。这是一种非常优雅的方式来约束系统行为，以用于开发的其余部分下一个细化将根“negative”事件deny根据访问权限进行拆分M. Benveniste/电子笔记在理论计算机科学280（2011）39R0=（rr1×BYs× {TyR}）（rw1× {TyW}）（ rx1×BYs× {TyX} ）（ rb1×BYs× {TyB} ）（re1×BYs× {TyE}）（AD×CL×BYs× {TyN}）见图6。 案例研究：固定r0的定义类型.它本来可以与第一个细化一起完成，但它会给自动机定义增加无用的复杂性。该细化还引入了一个本地堆栈，用于在嵌套中断的情况下管理清除级别。矩阵rb1和re1在这个阶段使用栈顶（空的或满的）和在前面的精化中引入的自动机的状态3.2架构层级然后介绍了体系结构级别的详细信息例如，主机微控制器的存储器映射用于划分地址集合，并且安全策略一方面专用于寄存器地址，另一方面专用于存储器地址。相应地，矩阵rr1、rw1和rx1由包含适当地址的表达式定义，尽管这些表达式中的一些尚未完全定义。它们将在稍后的阶段被定义。这就是这种精炼技术的本质。接下来的两个改进分别处理数据和代码的访问策略。矩阵rr4（rr1的一部分）和rw4（rw1的一部分）在数据访问策略中得到了更精确的定义，引入了（新的）矩阵rr5和rw5，它们将在后面的阶段中得到定义。正如对于r0，rr4（resp. rw4）和rr5（分别rw5）完全定义。这同样适用于矩阵rx4（rx1的一部分）以及在第七个精化中引入的定义它的关系和集合3.3执行层面实现细节将在以下细化中出现。我们成功的改进计划的关键点之一是，尽管我们处理的是地址，但我们设法避开了算术。 我们推迟了算术的使用，直到定义了参数化整个发展的具体常数。这就是为什么在图2中，提供所有常数赋值的文件是B4SYN的输入，B4SYN是用于将B合成为VHDL的特定翻译器[4]。这里的“诀窍”是依靠VHDL的类型检查和正确使用 而对于事件B更倾向于集合论。实际上，VHDL中用于综合的基本数据类型是std_logic_vector，它表示二进制和2的幂的集合10M. Benveniste/电子笔记在理论计算机科学280（2011）3本文首先介绍了案例研究的主要概念--分段，即分段的概念。一个可访问的地址窗口，通过单独使用集合（给定集合SE）。 首先作为一组地址（sa7）引入，见例3.2，它们变成了指定有起始地址和结束地址的地址范围的集合。他们最终被定义为开始和结束地址寄存器。例3.2[案例研究：作为地址集的段]sa7∈SE参与者AD让我们提到我们使用的建设性的集合表达式铺平道路的VHDL翻译，可以合成。例如，假设ms7是映射段的集合，我们可以使用例3.3中所示的表达式构建与给定地址a0相关联的段的集合ea7。例3.3[案例研究：构造性集合表达式]ea7={xa |xa ∈ SE <$xa ∈ ms7 <$（xa <$→ a0）∈ sa7}这些表达式在逻辑上等价于B和ML等函数语言中的let表达式。当使用足够简单的谓词时，它们平滑地转化为组合逻辑。另外两个细化阶段使我们能够精确地识别每个违规警报位需要设置的条件同样，报警寄存器也是由Event-B中的一个设置值变量建模的。设置和清除一个报警位为集合联合和集合差异操作提供代码，就像测试一个位值为报警成员的谓词提供代码一样容易。这在图7中示出，其中在alm8中出现未映射警报，因为对不属于任何映射段的地址进行了读访问，而不是异常的一部分。.alm8--.拒绝读取内存取消映射引用拒绝读取内存=选择M0= 2Tyt0=TyRa0∈MA（a0∈IVs7=然后m0：= 0|| v0 := TRUE|| alm8 := alm8 ∪ {Unmap}端图第七章案例研究：报警寄存器建模为集合我们亦小心避免过早定义将成为寄存器及╱或输出的变量的修改，以避免在优化期间进行复杂的证明工作。修饰语只表示尽可能长的“变成这样”的替代。它们在最后三个修正中成为具体的修正。为了使校对工作易于管理，请读取（生成输出）和写入（修改M. Benveniste/电子笔记在理论计算机科学280（2011）311寄存器）操作在单独的细化阶段变得具体。有效的读写操作通过常量函数引入，常量函数明确定义了主机和开发中电路之间的功能接口，参见图8中的状态1b和锁定。事实上，在Event-B开发中自然使用常量有助于完全分离功能和主机接口之间的关系通过这种分离在传统的VHDL编写中并没有广泛实践.状态1b∈ P（ALM）→BYslock∈BYs→BOOL.读取状态1=选择m0= 2<$t0 =TyR<$c0∈p4<$a0∈A3Ds<$b13=BdS1然后m0，v0，out13：= 0，v0，status1b（alm8）结束语：写锁=选择m0= 2<$t0 =TyW<$c0=ClSy<$a0∈A3Ds<$b13=BdL然后m0，v0，l4：= 0，m，lock（d0）端见图8。 案例研究：使用访问器连接到主机3.4真实界面最后一个改进引入了电路的物理接口，因为它嵌入到所选的主机微控制器中。这种改进突出地说明了B技术的传入线的值的每个组合我们主张将这种对应写在不变量中，以便事件精化的具体替换得到不变性证明义务的交叉检查。当接口变得更复杂时，这种冗余被证明是非常有用的。此外，可以想象使用这个不变量作为断言来监视主机系统，如[6]中所报告的那样。请注意，coverage属性将确保所有可能的输入组合都有一个关联的事件，而exclusiveness属性将确保每个关联的事件都是唯一的。为了总结这些小节，所选择的精化策略清楚地表明，谓词逻辑、集合运算、关系和函数是比乍一看更接近电路的二进制逻辑的概念。3.5生成VHDL改进后的模型已经足够接近一个明确的实现。最后一级的细化通过使用B4SYN[4]、常量赋值文件和转换器配置文件转换为VHDL模块，该转换器配置文件指示输入、输出、时钟和同步事件的列表。所产生的12M. Benveniste/电子笔记在理论计算机科学280（2011）3..（m0/= 0μ m）（t1 = TyR）⇔（（PSEL<$→PENABLE<$→PWRITE）=（TRUE<$→TRUE<$→）（m0/=0（t1 = TyW⇔（（PSEL<$→PENABLE<$→PWRITE）=（TRUE›→TRUE›→TRUE）））..phi读取参考phi=选择m0= 0∧RESET=FALSECLK=TRUE选择 PSEL=TRUE可忽略=真PWRITE=m0，a1，t1：= 1，PADDR，TyR结束语：phi write ref phi=选择m0= 0∧RESET=FALSECLK=TRUE选择 PSEL=TRUE可忽略=真则验证符=真m0，a1，d1，t1：= 1，PADDR，PWDATA，TyW端见图9。 案例研究：将数据线连接到事件VHDL可以直接合成，并且由于B4 SYN保留了Event-B语义4，因此该VHDL源代码是原始抽象函数基本属性3.1的经证明的正确构造实现。所产生的VHDL源代码现在可以安全地集成到经典的编程流程中，用于电路开发的其余部分。 由设计师执行并由Atelier B [3]记录的所有证明工作仍然是任何第三方查询电路功能正确性的可交付证据。事实上，这些履行的证明义务正式确定了所有设计决策的正确性原理，这些设计决策在功能开发中找到了自己的方式。我们的案例研究需要大约18个开发阶段，为5000个基本门的最终网络列表生成大约1600个证明义务。将获得的VHDL模块提交给该功能的传统定义中可用的验证活动，所有测试在RTL级和门级均达到通过结论，从而确认活动覆盖范围内的主机级行为不可区分所有这些工作都经过了安全评估机构的评估，并为法国认证机构ANSSI颁发的世界上第一个EAL6+通用标准3.1认证做出了贡献4从正确性到健壮性众所周知，正确的设计不一定是安全的设计，然而，反之亦然。我们的实验流程使用了正确性改进4 工作尚未完成。M. Benveniste/电子笔记在理论计算机科学280（2011）313通常，关系不能保持安全属性，如机密性或完整性。这绝不是拟议的预算草案的一个严重缺点。我们坚信，替代的特定形式化方法及其相关工具集应该在每个开发步骤中用于解决这些属性。虽然以下出版物不是最近的，但我们可以参考读者[5]，一种验证密码协议的实用方法，[10，8]用于基于原始组织的访问控制模型及其在网络安全策略中的应用，[22]用于通过静态程序分析技术实施信息流策略（如完整性或保密性）的调查，或[20]用于在进程代数细化下可以保留的非干扰公式，以及许多其他致力于安全属性的相关工作然而，在实践中，一些安全属性确实可以通过我们提出的方法来处理。以诚信为例。所提出的开发流程使潜在的执行模型，即基本门，是一个完美的设备的沉默假设。请注意，这个假设也存在于所有数字电路的源代码描述中，即在所有当前的开发流程中。现实生活告诉我们，否则：实验室的经验表明，积木式设备并不完美，并受到各种破坏，无论是意外或恶意性质。例如，通过数字电路环境的受控攻击，可以将基本逻辑（即易失性）存储器元件-Event-B的标准语义排除了这种错误行为，因此我们提出的Bulletow没有很好地提到这种完整性损失。我们称之为鲁棒性问题。图10给出了一个用Event-B编写的寄存器组（或寄存器）的模型。 它由复位值Q1和逻辑地址A1参数化. 在写入reg事件时，所呈现的输入d1被存储到其状态变量q1中。 就像我们在前面的案例研究中所做的那样，我们将输出变量的显式引入推迟到稍后的细化阶段，因此在读取reg事件时，不会发生可观察到的修改，但最后存储的值q1可用于输出。最后一个事件none表示不相关的访问，即不是对该地址的访问，也不是读或写。我们可以通过明确地对中断进行建模来将这些问题引入我们的开发中，如下所示：简单地将每个赋值替换为正确赋值和“变为任何值”命令之间的非确定性选择。这条路，虽然有趣的描述鲁棒性属性，碰巧是一个死-结束构造任何所需的函数，因为遵循它将允许我们制造一个随机失效的装置我们遵循的第二个简单的想法源于这样一种观察：一旦确定了导致完整性损失的故障模式，安全电路设计师就别无选择，只能构建对策。这个反措施是设计好的，最后，它碰巧只是另一个功能！对于手头的IPv6-IPv6示例，它可能是某种冗余的信息管理功能，因此从外部强制改变易受攻击的14M. Benveniste/电子笔记在理论计算机科学280（2011）3精制品01a精制品00a集ADs;BYs;TYs={TyR，TyW，TyN}抽象常数A 1，Q 1性质A 1∈ADs<$Q 1∈BYs变量m0，a1，d1，t1，q1不变量a1∈ ADs< $d1∈ BYs <$t1∈TYs< $q1∈ BYs初始化m0：= 0 ||a1：∈AD||d1：∈BYs||t1：∈TYs||q1：∈BYs事件读取reg=选择m0=2a1=A1t1=TyR然后m0：= 0结束语：写reg=选择m0=2a1=A1t1=TyW然后m0，q1：= 0，d1结束语：无=选择m0= 2（a1=A1t1=TyN）然后m0：= 0结束结束图10. Event-B中的存储器组或寄存器的示例并在其实现冗余功能.通过这种方式，完整性损失无法避免，但可以检测到，因此可以通过硬件、固件或软件中的其他功能报告和处理4.1注重正确性对于我们的寄存器示例，我们首先引入预期的警报err0，最初未设置。事件writereg、read reg和none通过未设置警报的条件来加强其防护。我们引入一个冗余常数函数，实际上是一个双射，RED 2，在这个阶段是左未定义的，以及冗余状态变量q2。不变量将所有东西联系在一起，形式化了反措施意图，如图11所示。..不变q2∈ BYs..（q1<$→q2）∈RED 2bool（（q1<$→q2）/∈RED 2）见图11。 摘自register示例，其中包含预期的完整性损失对策现在，事件写入reg必须更新q2，以便保持不变式。 这可以通过冗余常数函数RED 2为其分配所呈现的输入d1的图像来容易地实现。当且仅当警报不断更新时，对策才有效，即它必须在电路的组合逻辑中实现。因此，我们的执行模型psi中的相应事件被细化以指定此警报M. Benveniste/电子笔记在理论计算机科学280（2011）315更新如图12所示。挑剔的读者一定已经注意到，所展示的不变量有点太强了，因为它只适用于未中断的电路。事实上，只要没有状态变量，即q1和q2，以不受控制的方式被修改，我们就可以证明警报从未被设置。这个精炼阶段可以证明这一点。下一个细化阶段，实际上是实现，稍微削弱了不变量，并引入了真正的总线接口。抽象常数A1、Q1和RED 2由具体常数来细化，这些常数相同，但在最终实现中有一个下标i用于赋值除此之外，警报上的条件从事件的保护，图12显示了最后一个改进的摘录。引入了一个辅助变量q3，用于转换设置警报的表达式;这种技术已经在例3.3中的代码中进行了说明。输出信号ERR FF只是报警。..不变.联系我们 FF∈ BOOL错误0=错误FF（m0/= 1）ERR FF=bool（（q1<$→q2）/∈RED 2 i））.事件psi=选择M0= 1然后m0：= 2||q3, ERR FF:(q3 = RED 2 i (q1) ∧ ERR FF =(bool (¬ (q3 = q2))))结束语：读取reg=选择m0=2a1=A 1it1=TyR然后m0，PRDATA：= 0，q1结束语：写reg=选择m0=2a1=A 1it1=TyW然后m0，q1，q2：= 0，d1，RED 2 i（d1）端..图12个。鲁棒寄存器实现示例摘录如前所述，这种模式没有能力注意到中断。因此，所实现的函数确实可以被证明是正确的。弱化不变量的主要原因是使其尽可能类似于伴随模型的不变量，其编写将在以下段落中解释4.2证明可靠性我们对图11中部分展示的模型编写了一个未实现的改进。我们丰富了它的故障模型及其相关的中断事件，以证明在这些精确的情况下的反措施的效率16M. Benveniste/电子笔记在理论计算机科学280（2011）3为此，我们求助于改变状态q1、其冗余q2和警报err0的变量。我们还引入了一个抽象的见证，以表示发生的中断，df3。我们设想的故障模型是一个只有一个状态变量被修改的模型。我们进一步强调，中断发生在组合逻辑变得稳定。任何数量的位都可以被修改，只要它们都属于同一个变量表示。这个故障模型是相当一般的，因为我们没有深入到故障是如何注入的细节，只集中在它的记忆效应，即状态或输出被观察修改的情况。我们不包括组合中断，但我们没有预见到任何技术限制，以建立一个故障模型，涵盖他们也。由此产生的改进部分见图13。不变量告诉我们，这正是我们的意图。请注意，在图12和图13中，形式化警报含义的谓词设计相似。..不变..df3=bool（（q3<$→p3）/∈RED 2）（df3=100）优惠（q1=q3<$q2=p3<$err0=err3））（m0= 1）err3=bool（（q3<$→p3）/∈RED 2））断言（（m0/= 1）df3=err3）事件破坏=选择m0=1df3=1则q3，df3：（q3∈BYs<$df3=bool（q3<$→p3/∈RED 2））结束语：psi=选择M0= 1然后m0，err3：= 2，bool（q3<$→p3/∈RED 2）结束语：read ok ref read reg=选择m0=2err3=a1=A1t1=TyR然后m0：= 0结束语：write ok ref write reg=选择m0=2a1=A1t1=TyWerr3=THENm0，q3，p3：= 0，d1，RED 2（d1）端..图13岁带中断的鲁棒寄存器示例摘录虽然它们没有在图13中显示，但我们在错误模型中引入了事件read ko，write ko和none ko，以满足覆盖属性，因为现在警报确实可以触发。相关的替换只是开始一个新的循环（m0为0），在下一个细化中，这三个事件合并成一个单一的错误事件，当中断不会发生时，这是一个“奇迹”，在同级可实现的M. Benveniste/电子笔记在理论计算机科学280（2011）317模型部分如图12所示。这个简单的例子清楚地表明了我们的观点：安全属性可以很好地（至少部分地）转化为功能需求，从而克服了关于安全保护的细化限制。我们成功地应用这种技术来丰富MPU案例研究开发的完整性属性，使不可侵犯的更新实现这种控制访问策略，考虑到当前国家的最先进的基础半导体技术的漏洞。我们在早期的实现阶段添加了功能冗余，在开发的其余阶段，只要冗余信息失去一致性，就会触发一个新的警报仅为了证明工作，细化的死端分支引入了一个总是可以触发的“中断”事件，其动作正是“变为任何值”命令。依次尝试了几种故障模式。每个考虑的故障模型（单比特故障、双故障等）通过适当地选择受该“中断”事件影响的变量来引入。我们还加强了不变谓词，以便证明义务形式化了这样一个事实，即任何一致性损失都不会触发新的警报事件。解除这些证明义务意味着，无论这些变量上的故障在尝试的故障模型中受到什么影响，正确的实现永远不会触发指定的警报。这条小路证明工作一劳永逸地确立了反措施功能的有效主开发分支中的常规证明工作只处理其实施的正确性[7，11]。总结本节，我们已经能够通过将鲁棒性问题分解为两个本质上不同的部分来规避所提出的流程的明显缺点(i) - 一个模型，用于陈述和证明所提议的对抗措施的功能描述的有效性，以阻止所提议的故障的影响;(ii) 一个模型以通过构造证明正确的方式构建所提出的函数，两个模型都是原始脆弱函数的改进5一个被转移的用途来验证算法除了鲁棒性之外，安全微控制器还需要非常谨慎，在执行密码操作时不受约束。事实上，功率分析[26]提供了非常强大的技术来从电路操作的物理特性（通常是功耗）中提取秘密（通常是加密密钥）。因此，安全微控制器的加密加速器的设计必须集成反措施，以减轻对这些不可避免的观察的利用。设计从描述算法开始，通常是标准算法[16，15，21]。对于其中一些算法，已知理想的安全属性会显著阻碍功率分析的成功。例如，在对称密钥算法[16，15]的情况下，必须在电路的最终布局中满足性质5.118M. Benveniste/电子笔记在理论计算机科学280（2011）3定义5.1[安全属性]任何依赖于输入消息和密钥的值都必须用随机数进行掩码虽然正确性保持并不意味着开发中的保密性保持，但如果算法的详细描述违反了该属性，最终布局也将以接近确定性的概率违反它。第三个简单的想法使我们能够对设计师提出的详细算法进行分析。观察到所需的属性5.1涉及的值之间的依赖关系多于实际数据值，我们使用抽象解释[24]手动转码5详细算法，将其域从数据更改为依赖关系。所使用的抽象集中在敏感数据上的掩蔽和反掩蔽操作。该变换如图14所示，其中对两个寄存器的内容D1和D2执行操作Op，这两个寄存器分别由随机数m1和m2掩蔽6。接口输出寄存器（标记为reg o）从左侧数据路径（标记为lmux，未使用m1屏蔽）获取其值，即值D1=（D1m1）m1，或者根据多路复用器设置（即左或右位置）获取常数值0。见图14。 从如[19]中所报告的，我们编写了一个Event-B（Eventat）系统来表示每条线上和每个寄存器中的依赖关系集，在分析的详细算法的每个时钟步骤之后观察到。我们为这个模型配备了每个所需属性的不变量。仅为了提供所得到的事件B系统的概述，图14中所示的详细算法数据路径的摘录用于编写小的对应事件B系统。它在图15中提供。回到图14中的示例，敏感数据是同时依赖于输入消息和密钥的数据。在第一个近似中，输入消息和键被两个不同的常量依赖标签I和K7抽象。5 这一步骤的严格性可以通过自动化来提高。6掩码操作是按位异 或、 异或、异或。7在图15的事件B系统中，D1和D2本身被认为是敏感数据M. Benveniste/电子笔记在理论计算机科学280（2011）319系统电子数据处理部定义MASKS=={M1，M2};XOR（A，B）==（A）（B））-（（A）（B）MASKS））;SECRET==P1（{D1，D2}）;REGDEPs=={drego，dreg1，dregr，dreg3};敏感的总是掩盖==（秘密的REGDEPs=）集DEPs={D1，D2，M1，M2};MUXPOS={LP，RP}变量dreg1，dregr，dreg3，dlmux，muxpos不变∈BOOLdreg3步骤1. 17电子邮件 始终戴面具初始化，step：=TRUE，1|| muxpos：∈MUXPOS|| drego, dreg1, dregr, dreg3, dlmux:= ∅, ∅, ∅, ∅, ∅事件switch left=SELECTmuxpos=RP切换=TRUETHENmuxpos，dlmux，dlmux：=LP，dreg1，dlend;switch right=SELECTmuxpos=LP切换=TRUE然后muxpos，dlmux，dlmux：=RP，dlmux，dlmux：=RP，dlmux，dlmux结束;load reg1=SELECTstep= 1选择 =真那么dreg 1，step，step：={D1，M1}，step+1，step_END;load reg2=SELECTstep= 2选择 =真THENdregr，step，step：={D2，M2}，step+ 1，step_END;做操作和饲料=选择step= 3步骤 =TRUE THENdreg3，drego，step，step：=dreg1dregr，XOR（dlmux，{M1}），step+1，step_END;update wire left=SELECT左= SELECT左muxpos=LPTHENdlmux，NULL：=dreg1，TRUE END;update wire right=SELECT右= SELECT左muxpos=RPTHENdlmux，：=，TRUE END;其他步骤=选择步骤> 3步骤≤ 16步骤 =TRUETHEN，步骤：=，17结束;do cycle=SELECTstep> 16循环 =TRUE THEN循环，step：=1，1结束结束图15. 基于图14所示算法的事件B系统代码敏感数据由以下集合抽象(1) 秘密={I，K}掩码被抽象为唯一的常量依赖标签，即Z。该算法的每一个数据操作都被抽象成它对被操作数据的依赖性的结果。仍然参考图14，经验经验表明，Op是这样的，即在其输出中可以观察到对其两个输入的依赖性。因此，它被抽象为集合并集。用于取消屏蔽数据的异或操作被抽象为集合差异。每一条线和每一个寄存器都由一个变量来表示，这个变量保存着它当前的依赖关系。在图14中，这些变量标有导线的名称（分别为寄存器）前缀为d（用于依赖关系）。每一步都由两个事件的序列建模，因为我们需要观察寄存器和连接。一个事件表示寄存器的更新，另一个事件表示寄存器的所有输出线的稳定更新。安全属性5.1变为以下不变量（对于w线和r寄存器）：(2) secret/e {d线1，.，d线w，d寄存器1，.，d regr}我们使用模型检查器ProB [17]来验证是否所有属性都是20M. Benveniste/电子笔记在理论计算机科学280（2011）3详细的算法。我们发现模型检查器对于这种分析非常有效，因为每当违反属性时都会提供反例导致违规的每一步都被工具清楚地识别出来。参考图14，ProB8立即示出，当d_reg_r获得对屏蔽的敏感数据的依赖性并且多路复用器被设置到左侧时，由于d_reg_o的线输入获得秘密依赖性，因此违反了属性2这对我们大多数人来说似乎微不足道，但对真正详细的算法进行验证揭示了非常棘手的情况，只有非常彻底的分析才能发现。此外，我们能够提出一个改进的详细算法。我们说服设计者实现它，通过展示提出的修改，ProB可以完成所有属性的详尽验证。虽然我们的发现对所研究算法的发展产生了直接影响，但这种方法还不能被视为一种实用的解决方案，而是邀请研究界研究这些新的转移方法，将抽象解释和证明和/或模型检查结合起来，以解决复杂系统的不同方面。6结束语和前进的虽然通过大量的案例研究，已经明确了数字电路的结构验证开发流程的可行性，但鉴于以下问题需要大量的进一步工作，我们必须缓和我们的热情• 通过同样大量的案例研究，已经表明稳健性问题可以接受方便的类似函数的处理，但既没有系统的过程，也没有合理的基础理论来考虑解决问题;• 安全微控制器的安全性的一个整体部分甚至没有在建议的流程中被考虑：事实上，如所解释的，保密问题并不像我们使用的那样以保守的方式与细化关系一起表现。我们已经暗示了使用其他专门的形式化方法来处理这些问题，但仍需要研究各种专门的形式化方法以• 最后，可行性只是部署新技术的第一步。 许多工程、技术、经济和人类问题有待解决，以便将数字电路的安全建设开发流程扩大到工业用途。8ProB完全集成在Atelier B和罗丹[18]中。M. Benveniste/电子笔记在理论计算机科学280（2011）321确认如果没有Louis Mussat的杰出工作，这个实验是不可能成功的，他开发了最初的事件B模型和案例研究的相关证明。Thierry Lecomte和Antoine Requet设计并实现了B4SYN翻译器，并将其集成到Atelier B中[3]。愿他们在这短短几行字中读到对他们对该项目的巨大贡献的感谢。我还要感谢Marie-Laure Potet对本文初稿的建设性评论，并感谢研讨会计划委员会成员对这项工作的兴趣引用[1] Abrial，J.- R.，“ModelinginEvent-B”，剑桥大学出版社，2010年。[2] Abrial，J.-R.，[3] “http://www.atelierb.eu/indexAtelier B”，www.example.com en.html.[4] Benveniste ， M. ， 一个正确 的结构现实 数字电路 ，RIAB 研讨会 ，FMWeek 2009 ，埃 因霍 温，handout.pdf。[5] Bolignano，D.，Towards a Mechanization of Cryptographic Protocol Verification，in CAV[6] Borrione，D.，M. Liu，P. Ostier，L. Fesquet，基于PSL-based的数字系统在线监控，在A。Vachoux（ed.） 2（2006），5[7] 欧洲共同体委员会理事会XIII/F SOG-IS，[8] 来 吧 ， 弗 。 、 N.Cuppens-Boulahia ， T.旧 金 山 和 华 盛 顿 。Mi`ege ， AForma l Approac htoSpecifyandDeploya Network Security Policy，in Second IFIP Workshop on Formal Aspects in Securityand Trust（FAST），203 -218，2004，[pdf].[9] EE Herald，New products，5 November 2010，[Web page].[10] ELKAMAL. 一、 R. ElBaida，P. Bal b iani，S. Benferhat，F. 杯子，Y。 Deswarte，A. 米埃盖角所以rel和G. 张文龙，基于组织的访问控制，第四届I