On Using B in the Design of Secure Micro-controllers: An Experience Report
Abstract
The stepwise formal development of safety critical software is now a well established engineering practice,noticeably in railway systems. However, it has not been applied as successfully to hardware development, where formal methods are mainly used for verification and gate level transformations and optimizations. In this paper, we report our recent experience in the stepwise formal development of a real macro-cell, that opens the way to the design of synchronous digital circuits with zero functional bugs. We propose a development flow suited for obtaining proven correct-by-construction circuits that further possess additional robustness properties desirable for secure chips. The reported work is prospective and is meant to show the feasibility of such a technique for high confidence trustful devices.
Keywords: formal development flow, digital circuit, robustness, secure micro-controller, correct by construction.
1 Introduction
The first contribution of this work shows the feasibility of a stepwise transformation of a formal security policy model into a synthesize-able hardware description of the security functionality that implements it.
The second contribution of this work enhances the experimental formal development flow so that robustness properties can also be handled in a proven way.
The third contribution of this work is an experimental combination of abstract interpretation and model checking to verify a given set of properties on an algorithm before any attempt to implement it.
Finally, we report on unsolved issues that have been identified and that call for further research and development work.
2 Towards a formal development flow
A traditional development flow for digital circuits heavily relies on testing for the verification steps performed before launching the manufacturing process in a foundry. Figure 1 below presents a schematic view of the main artefacts used during the first steps of a typical micro-controller function development.
Fig. 1. First steps of the development flow of a digital function for a micro-controller circuit Writing test programs, running and analysing simulations, represent a preponderant part of this first development effort. The verification plan is solely built upon expertise and experience of specialized designers. Coverage of a verification campaign is measured by using some specialized tools, but functional specification coverage is at best mainly a matter of peer review: the only available reference is the natural language description of the function to be designed.
A simple idea roots our work. Looking at a safety-critical software development widely recognized as a success story, i.e. the Paris Macute;etro Line 14 automated system [25], it can be noticed that verification was performed all along the development through the use of the stepwise refinement methodology underpinning the B technology [2].
The simple idea was to adapt this B formal method to the development of our digital circuits. Indeed, microelectronics development tools already resort to many formal methods, but they are used mainly behind scenes, i.e. without designer awareness of their presence, and more importantly, their application only starts after the source code has been written. These methods are used for verification purpose and for various transformations in the long path leading from a Register Transfer Level (RTL) representation to a final placed and routed net list. Nevertheless, the more expensive functional errors are often introduced before the first line of code is even written. Usually they stem from the functional, the high-level design, or even the detailed design specifications. As already mentioned, no verification tool is available for these natural language representations. Only a thorough peer review can possibly filter out these error seeds before they blossom into forests of erroneous behaviours, once embedded into the circuit.
We defined, and experienced on a use case [4], a new development flow that makes extensive use of formal proof and produces an exhaustively verified source code both in its functional behaviour and in its interface definition (see figure 2). This source code, actually VHDL, can directly be synthesized. It has therefore the capability to enter the rest of the standard industrial flow untouched.
This experimental development flow relies on a formal model of the required function expressed in Event-B [1], a recent evolution of the B Method targeting system development. We believe that this new flow can be used to build any digital function in a proven correct-by-construction way. Analogue functions fall out of the scope of these techniques, but their digital interfaces are used as a formal correctness contract in order to include them in the otherwise proven digital circuit.
Fig. 2. The proposed development flow, as defined and experienced on a case study
3 Results
The proposed flow begins with a huge abstraction step. The designer must write an Event-B model of only a few lines that captures the essential property of the function to be designed. Achieving this goal is no easy task. Many trials are required even for a highly trained engineer. Just be reminded that simplicity is almost always very hard to achieve.
The case study we experienced with was no exception. We had to struggle a while before stating the following:
Definition 3.1 [Essential Property] The essential property of a memory protection
unit is to monitor all accesses a microprocessor performs. This function is central to the access control security policy to be implemented on the secure micro-controller as illustrated in figure 3.
Fig. 3. Case st
剩余内容已隐藏，支付完成后下载完整资料
在安全微控制器设计中使用B：经验报告
摘 要
安全关键软件的逐步正式开发是一个成熟的工程实践，特别是铁路系统。然而，它并没有成功地应用于硬件开发，形式化方法主要用于验证和门级转换和优化。
在本文中，我们报告最近的经验，在一个真正的宏单元的逐步正式发展，这开辟了同步数字电路设计与零功能错误的方式。我们提出了一个开发流程，适合正确的建设电路，进一步拥有额外的安全芯片所需的特性。报告的工作是前瞻性的，是为了显示这种高信任设备的可行性技术。
关键词：正式开发流程，数字电路，鲁棒性，安全微控制器，校正建设。
1引言
这项工作的第一个贡献表明逐步变换的可行性一个正式的安全策略模型到一个综合硬件描述实现它的安全功能。这项工作的第二个贡献增强了实验的正式开发流程，使鲁棒性属性也可以以一种行之有效的方式处理。这项工作的第三个贡献是抽象的实验组合解释和模型检查，以验证给定的一组属性的算法在任何尝试实施它。最后，我们报告尚未解决的问题，已确定和调用进一步的研究和开发工作。
2走向正式开发流程
传统的数字电路开发流程很大程度上依赖于在铸造车间推出制造工艺之前进行的验证步骤的测试。下面的图1给出了一个典型的微控制器功能开发的第一个步骤中使用的主要文物示意图。
图1。微控制器电路数字功能开发流程的第一步
编写测试程序，运行和分析模拟，这是第一个发展努力的优势部分。验证计划完全建立在专业设计师的专业知识和经验之上。验证活动的覆盖范围是通过使用一些专门的工具，但功能规格的覆盖范围是最好的，主要是一个同行评审的问题：唯一可用的参考是要设计的功能的自然语言描述。
一个简单的思想根源于我们的工作。寻找一个安全关键软件开发被公认为一个成功的故事，即巴黎Macute;Etro 14线自动化系统[ 25 ]，它可以发现验证始终是发展通过逐步求精的方法对B技术[ 2 ]使用进行。
简单的想法是，以适应这种B形式的方法，我们的数字电路的发展。事实上，微电子开发工具已经采取了许多正式的方法，但它们主要用于幕后，即没有设计师意识他们的存在，更重要的是，他们的应用程序只有在源代码已被写入。这些方法用于验证的目的和各种变换的长路径从寄存器传输级（RTL）表示最终放置和路由的网络列表。然而，更昂贵的功能错误往往被引入前的第一行代码甚至写。通常它们源于功能，高层次的设计，甚至详细的设计规范。如前所述，没有验证工具可用于这些自然语言表示。只有彻底的同行评审，才能过滤掉这些错误的种子，然后再进入错误行为的森林，一旦嵌入到电路。
我们定义，并经历了一个用例[ 4 ]，一个新的开发流程，使广泛使用的正式证明，并产生详尽的验证源代码无论是在其功能的行为和它的接口定义（见图2）。这个源代码，实际上是VHDL，可以直接合成。因此，能够进入标准工业触及流动的休息。本实验开发的流量依赖于所需的功能在Event-B [ 1 ]表示一个正式的模型，最近的一个进化的方法定位系统的开发。我们相信，这种新的流量可以用来建立任何数字功能在一个行之有效的正确的施工方法。模拟功能下降的范围，这些技术，但他们的数字接口作为一个正式的正确性合同，以包括他们在其他证明的数字电路。
图2。建议的开发流程，定义和经验的案例研究
3结果
建议的流程开始与一个巨大的抽象步骤。设计者必须写只有几行，抓住了本质属性事件-B模型设计功能。实现这一目标并非易事。需要许多试验即使是训练有素的工程师。只是提醒，简单几乎总是很难实现。我们所经历的案例研究也不例外。我们不得不斗争在此之前说明以下：
定义3.1 [本质属性]存储器保护的本质属性
单元是监视微处理器执行的所有访问。此功能是在安全微控制器上实现的访问控制安全策略的中心，如图3所示。
图3。安全微控制器存储器保护单元的研究
初始属性级模型以简化的方式在图4中给出。设计功能的实现细节逐渐介绍嵌入到主机的微控制器。细化的主要策略计划是逐步定义和变换表示访问权限的变量矩阵，R0。双重转变是引导一方面，通过介绍不同类型的访问及其相关细节，另一方面，由权利矩阵的实现表示。应该指出的是，我们细化路径受限于已经实现所需功能的遗留模块的存在。这就是为什么接口规范和数据表的章节被标识为图2中的开发流程的输入：前者提供的模块和总线协议的线电平接口后者定义寄存器地址、名字、函数、位意义程序员指导。一个定时器描述的例子嵌入在通用微控制器公共数据表[ 23 ]如图5所示。各种细化的途径和策略进行了尝试，往往导致一个死胡同或复杂的情况将成为压倒性的证据。
图4。案例研究：初始属性级模型
我们终于建立了细化计划有两个重要的“没有”属性：没有损失覆盖和没有非决定论。事实上，因为这个时钟电路必须有对于任何输入组合在每个循环定义的行为，事件B模型必须实现一个完全确定性函数：
bull;其事件的警卫析取必须空虚的真。此外，我们强加的，没有“漏洞”时，可以引入细化事件。每当（摘要）事件的EA是成品（分裂）的（具体的）事件ECI，如果分离具体事件的守卫是由抽象事件的守卫所暗示的，我们可以肯定的是，没有“案件”已被发现。以双重方式，无论何时（摘要）事件EAI是由（具体的）事件EC细化（分组）的，我们必须证明具体事件的守卫是由抽象的析取暗示的事件守卫。我们称此属性为覆盖属性；
bull;非确定性行为禁止微控制器。我们必须确保事件成对独占。我们称这个属性为排他性的财产。实施这些属性是通过生成额外的在事件B系统工程工具工作室B [ 3 ]证明义务。请注意，在每个细化阶段证明这些属性减少了总数的证明义务，排他性的财产，组合性质明显。为了提供一个风味的战略，我们建议发展数字电路，主要细化阶段，在下面的段落。
图5。案例研究：一个数据表层次描述的例子，这里有一个定时器寄存器
3.1个层次
第一细化介绍不同类型的访问，如阅读（Tyr）写（tyw）的数据，取（TYX）代码，中断（TYB）开始和结束中断（型），并不能访问（TyN）。后者最初被遗忘，但覆盖证明义务。这些事件都是根“正”事件允许。访问矩阵模型更精确地定义为矩阵的集合，每个访问类型的一个。每个矩阵都是左现阶段未定义。他们的关系完全定义了R0下一个细化介绍了自动机，驱动一些例外情况下中断和复位的主机微控制器的条件。只有状态自动机和由相关事件执行的转换保持在下一步细化。这是一个相当优雅的方式来约束系统行为其余的发展。下一步细化根“否定”事件拒绝根据访问。
图6。案例研究：不变的锚固R0的定义型。
它本来可以一起做的第一个细化，但它会有增加了无用的复杂性自动机定义。这种细化的介绍也有一个本地堆栈管理间隙水平的情况下，嵌套中断。矩阵Rb1和Rg1能完全定义在这个阶段使用栈顶（空或满）在以前的精化中引入自动机的状态。
3.2建筑水平
架构级别的详细信息，然后介绍。例如，内存映射的主机微控制器用于分区的地址集和安全策略一方面专门用于寄存器地址，另一方面用于内存地址。相应地，矩阵RR1、RW1和RX1定义的表达式涉及足够的地址，即使有些表达式不是尚未完全定义。他们将在稍后的阶段定义。这就是这个的本质细化技术。接下来的两个改进分别处理数据的访问策略和用于代码。矩阵RR4（部分RR1）和RW4（部分1）得到更精确用于数据访问策略定义，引入（新）矩阵RR5和rw5将后期定义。只是为R0，之间的关系（或4。RW4）和RR5（或。rw5）完全定义。矩阵rx4同样（部分RX1）和第七次细化中定义的关系和集合。
3.3实施水平
实施细节使其出现在以下改进。一我们成功的细化计划的关键点是我们设法保持算术虽然我们在处理地址。我们推迟了使用算术到具体的常数参数化整个的定义发展。这就是为什么在图2中，该文件提供了所有的估值常数的b4syn输入，具体翻译成B的合成VHDL [ 4 ]。这里的“窍门”是依靠VHDL的类型检查和正确使用算术而宁愿event-b.集理论的确，基本数据类型VHDL合成是std_logic_vector表示数二进制基数和2幂集。
我们介绍了案例研究的主要概念，段，即可访问地址窗口，通过唯一使用的集（给定集SEs）。首先介绍了作为一个组地址（SA7），见例3.2，他们成了组地址范围指定一个开始和结束地址。他们最终被提炼来定义通过开始和结束地址寄存器。
案例3.2 [案例研究：段为一套地址]
SA7isin;SESharr;Ads
让我们提到我们使用建设性的表达方式铺平了道路可以合成的VHDL翻译。例如，让数据设定映射的部分，我们可以建立EA7段关联到一个给定的地址A0与表达式如图3.3所示。
例3.3 [案例研究：建设性集表达式]
EA7 = { XA | XAisin;SESand;XAisin;MS7and;（XA→A0）isin;SA7 }
这些表达式在逻辑上相当于让表达式在B和函数语言如ML [ 14 ]。他们顺利地转化为组合逻辑当使用简单的谓词时。两个细化阶段，使我们能够准确地识别条件下每一个违规报警位都需要设置。再次，报警寄存器是简单模拟的集值变event-b.设置和清除报警位提供代码集并集和设置差分操作一样容易测试位值为告警成员的谓词提供代码。这说明图7在未报警是上升alm8因为读访问，不异常的一部分，由不属于任何映射的地址构成段。
图7。案例研究：报警寄存器建模为一套
我们也小心不要定义修改的变量必然成为寄存器和/或输出过早避免复杂的证明工作在细化。修改只表示与“成为这样的”替代为尽可能长。他们在三个最后的改进变得具体的修改。保持证明工作的可管理性，阅读（生成输出）和写入（修改）寄存器在具体细化阶段得到具体操作。有效的阅读并用常数函数明确地定义了写操作主机和正在开发的电路之间的功能接口，看到status1b并锁定图8。事实上，在事件B发展自然使用常数促进功能和主机接口之间的完全分离通过“访问器”常数。这种分离在传统中没有得到广泛的应用VHDL编写。
图8。案例研究：使用访问器接口到主机的关注点分离
3.4真正的接口
最后细化引入了物理接口的电路，因为它是嵌入式进入选定主机微控制器。这种细化突出地说明了“赋值方案的含义”B技术的本质[ 2 ]。每个组合传入的电线“代码”的语义事件之一的值，如图所示
图9。我们主张写这个对应的不变，使
事件替换的具体替换通过不变性证明义务得到交叉检查。当接口变得更复杂，这种冗余证明非常有用的。此外，我们可以想象使用这个不变量作为断言来监视主机系统报告[ 6 ]。要提醒的是，覆盖财产将确保所有可能的输入组合有关联事件，并且互斥属性将确保每个关联事件都是唯一的。为了总结这些小节，所选择的细化策略清楚地表明谓词逻辑、集合运算、关系和函数是概念对于电路的二进制逻辑，它可能会出现在第一眼。
3.5生成VHDL
精致的模型已经接近到一个明确的实施。这个细化上的高低是由b4syn [ 4 ]利用转化为VHDL模块，常量赋值文件和一个译者配置文件，表示其他，输入，输出，时钟和同步事件列表。
图9。案例研究：将电线分配到事件生成的VHDL可直接合成的，而b4syn保留Event-B语义4、本VHDL源代码是由建设实施证明是正确的
原始抽象函数本质属性3.1。所产生的VHDL源代码，现在可以安全地集成到经典的流程，其余的电路开发。所有的证明工作进行由设计师，并记录工作室B [ 3 ]，仍然作为可交付的证据任何第三方对该电路功能正确性的询问。的确,这些出院证明义务正式的正确性，所有的设计决定，找到自己的方式进入功能开发的理由。我们的案例研究需要大约18个发展阶段产生约1个600证明义务为5个基本门的顺序的最终净名单。得到的VHDL模块提交给验证活动可从这个功能的遗留开发和所有的测试都达到了在RTL级的通过判决并在门级，从而证实了一个无法区分的主机级行为竞选报道。所有这项工作已评估的安全评估设施和促成了世界上第一个EAL6 普通标准3.1证书，由法国认证机构颁发，安西[ 13,9 ]。
4从正确性到鲁棒性
众所周知，一个正确的设计并不一定是一个安全的设计，相反的是真实的，但是。我们的实验流程使用的正确性细化一般而言，未能保存诸如保密性等安全属性的关系或完整性。这决不是建议流动的严重缺陷。我们坚信，选择具体的形式化方法，及其相关的工具，可以用来在发展的每一步处理那些性质。虽然下面的出版物不是很新，我们可以参考读者[ 5 ]一种安全协议验证的实用方法，以[ 8 ]一基于原组织的访问控制模型及其在网络安全策略中的应用（22）：一个关于完整性信息流策略的调查通过静态程序分析技术或机密，或[ 20 ]为无为的配方，可以细化进程代数下保存，其中许多其他相关工作致力于安全性能。然而，一些安全属性，在实践中，确实可以处理由我们提出了流动。
以正直为例。建议的开发流程，使沉默的假设，底层执行模型，即基本的门，是一个完美的装置。请注意，这个假设也存在于所有源代码描述数字电路，即所有当前开发流程。现实生活教我们别的：实验室的经验表明，积木设备是不完美的，并受到各种干扰，他们是偶然的或恶意的性质。例如,触发器，基本逻辑（即易失性）存储元件，可以强制给定通过对数字电路环境[ 12 ]控制侵略的价值。这个对Event-B标准语义这种不当行为，因此排除我们建议的流程没有充分装备提到这种完整性损失。我们称它们为鲁棒性问题。一个模型，一个触发器的银行，或登记，写了事件B
图10。这是由其重置价值，Q 1，其逻辑地址1。在写寄存器事件，所提出的输入D1被存储到它的状态变量Q1。正如我们在以前的案例研究中，我们推迟明确的介绍输出变量到稍后的细化阶段，所以在读寄存器事件，没有观察到修改发生，但Q1，最后存储的值可用于输出。最后事件，没有，模型不相关的访问，即不到这个地址或不读或写。我们可以通过明确的建模引入这些问题到我们的发展中断如下：简单地替换每个赋值的非确定性正确赋值和“成为任意值”
剩余内容已隐藏，支付完成后下载完整资料
资料编号：[485417]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
