可证明安全的基于位置的Prover-to-Prover密钥交换协议

本文针对两个证明者之间可证明安全的基于位置密钥交换协议展开研究.首次将基于位置密钥交换分为P2V(Prover-to-Verifier)模式和P2P(Prover-to-Prover)模式,并给出P2P模式下基于位置密钥交换的安全定义.随后,在1维空间下设计了可证明安全的基于位置P2P密钥交换协议P2PKE1,并以此为基础构造了d(1≤d≤3)维空间下基于位置P2P密钥交换协议P2PKEd.同时,分别提出了具有密钥确认性质的基于位置P2P密钥交换协议P2PKEd-c和无密钥托管的基于位置P2P密钥交换协议P2PKEd-e.最后,从安全性和效率两方面对所设计的协议进行了讨论.

基于Tamarin Prover的5G EAP-TLS协议的形式化分析

为了保证5G专用网络中移动设备的通信安全,第三代合作伙伴计划(3rd generation partnership project,3GPP)提出了5G可扩展认证协议-传输层安全(extensible authentication protocol-transport layer security,EAP-TLS)。然而,现有的针对于5G EAP-TLS协议的研究工作较少且缺乏系统性。因此,对5G EAP-TLS协议进行详细的描述,并对该协议进行全面的形式化建模。对5G规范中涉及的所有协议实体以及证书分发机制进行建模,同时从5G规约中提取并建模了与5G EAPTLS协议相关的安全目标。提出证据搜索策略引导符号分析工具Tamarin Prover进行自动化证据搜索,解决了Tamarin Prover在验证复杂模型时验证过程无法终止的问题,实现了5G EAP-TLS安全目标的自动化验证。通过分析验证结果,发现了5G EAP-TLS协议能够满足机密性目标,但难以满足一些认证性目标,同时,揭示了协议存在拒绝服务(denial of service,DoS)攻击和用户通信数据泄露的隐患。针对发现的问题,提出了相应的补丁方案,并通过提出的证据搜索策略引导分析工具Tamarin Prover自动化验证了该补丁方案的有效性。

LLRB算法的函数式建模及其机械化验证

基于机器定理证明的形式化验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.LLRB(left-leaning red-black trees)是一种二叉搜索树变体,其结构比传统的红黑树添加了额外的左倾约束条件,在验证时无法使用常规的证明策略,需要更多的人工干预和努力,其正确性验证是一个公认的难题.为此,基于二叉搜索树类算法Isabelle验证框架,对其附加性质部分进行细化,并给出具体化的验证方案.在Isabelle中对LLRB插入和删除操作进行函数式建模,对其不变量进行模块化处理,并验证函数的正确性.这是首次在Isabelle中对函数式LLRB插入和删除算法进行机械化验证,相较于目前LLRB算法的Dafny验证,定理数由158减少至84,且无需构造中间断言,减轻了验证的负担;同时,为复杂树结构算法的函数式建模及验证提供了一定的参考价值.

矛盾体分离超演绎方法及应用

作为当前自动定理证明器中常用的推理机制,传统基于二元演绎超归结方法的推理过程限定每次有且只有2个子句参与演绎,这种分离的演绎步骤导致演绎缺失导向性和预判性,演绎效率有待提升。为了提升演绎效率,在理论上,针对传统的超归结方法引入多元演绎思想,提出矛盾体分离超演绎定义和方法,它具有多元性、动态性和导向性的演绎特性;在算法实现中,考虑子句参与演绎具有多元和协同特性,并灵活设定演绎的条件,提出一种具有回溯机制的矛盾体分离超演绎算法。将所提算法应用于Eprover3.1证明器,以国际自动定理证明器2023年竞赛例和TPTP(Thousands of Problems for Theorem Provers)问题库中难度系数为1的问题作为测试对象,在300 s内,应用所提算法的Eprover3.1证明器比原始Eprover3.1多证明了15个定理;当测试相同数量的定理时,所提算法的平均证明时间缩减了1.326 s,能够证明7个难度系数为1的定理。测试结果表明,所提算法能有效地应用于一阶逻辑自动定理证明,提升自动定理证明器的证明能力和效率。

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑,操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障,造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生,对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误,因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中,互斥量可协调多任务对资源的访问,是一种常用的任务同步方式,其功能正确性对于保障多任务应用的正确性十分关键.基于定理证明方法,在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模,给出其接口函数的形式化规范,并实现这些接口函数的功能正确性验证.

钟罩式气体流量标准装置温度梯度影响研究

钟罩内部封闭气体稳态条件下的温度分布可用拉普拉斯方程描述,边界等温时温度为竖向一维直线方程梯度分布。建立坐标系,将钟罩位置绝对编码,两点测温法获取直线方程。考虑湿度影响导出非线性一维分布气体密度函数,进行空间积分,获钟罩任意高度区间气体质量函数,进而导出质量流量函数。当气体流动满足绝热等熵过程时,根据连续性方程导出流量计处状态下仅关于压力的体积流量函数,有效解决温度测量响应滞后问题。实例计算表明,以点温度代替梯度温度会使钟罩排出气体的质量引入显著的系统误差,必须对密度按空间积分加以修正。

基于二幂阶矩阵的量子中间表示与翻译

在两能级量子计算系统中,所有量子门、量子态和测量算子都可以表示为2的幂次方阶矩阵(简称二幂阶矩阵)的形式,而现有量子编程语言未考虑该特性。因此,提出一种二幂阶矩阵类型系统,并设计相应的量子中间表示。首先,在定理证明器Coq中利用递归对偶结构实现二幂阶矩阵系统,可以精确描述量子门、量子态和测量算子;其次,设计一套量子中间表示作为编程工具,可以自动将量子程序翻译为二幂阶矩阵表达式;最后,展示量子傅里叶变换的编写和翻译过程。二幂阶矩阵系统为基于定理证明器的量子编程语言提供了更精确、更简洁的类型系统,量子中间表示实现了从二幂阶矩阵到程序语言的过渡,提供了在二幂阶矩阵系统中编写量子程序的有效手段。

基于定理证明器的行波进位加法器开发以及新的芯片设计方法探索

数字芯片的规模已经进入几百亿晶体管的时代,传统的硬件设计方法难以应对日益复杂的电路需求,比如基于Verilog语言的硬件设计。针对这个问题,文章以行波进位加法器为例,探索基于交互式定理证明器Coq的芯片设计方法,该方法不仅在Coq中完成了加法器的RTL描述,而且进行了加法器的功能仿真、形式验证、Verilog代码生成、网表生成和网表仿真。这个案例在单一的编程平台里把RTL设计同前端EDA的主要流程整合在一起,虽然案例简单,但可以初步体现出基于Coq的芯片前端设计的可能性,并且希望能够从此出发探索出新的基于定理证明器的芯片设计流程。文章的主要技术路线是在Coq中开发芯片设计的抽象语法树,然后基于这个抽象语法树展开行波进位加法器的前端开发流程。实验结果表明,Coq在支撑芯片设计方面有巨大的潜力,并且基于定理证明器的验证是可以复用的,这有利于验证大规模的系统。尽管这一方法处于探索阶段,但它为未来的芯片前端设计提供了全新的思路,有希望发展成为一种新型的芯片前端设计方法。

尺寸法测量活塞式体积管标准装置标准容积的不确定度评定

活塞式体积管主要用于石油产品等液体流量的计量,一般通过容积法溯源,受限于上级标准二等金属量器准确度等级。通过容积法测量体积管标准已达技术瓶颈,测量不确定度难以提升。为进一步提高活塞式体积管标准装置的测量准确度,以达到油流量原级标准技术水平,针对该装置自身结构特点,改变惯用溯源方式,提出了尺寸法测量标准容积的方法,即精密测量体积管标准段内径和检测开关间距离,从而计算得到标准容积,将体积量溯源至长度基准,减少溯源环节并提高测量不确定度。建立尺寸法数学模型,分析影响该测量方法不确定度的4个来源,即内径测量、长度测量、线膨胀系数、温度测量,并具体分述和评定了这4个分量,对尺寸法测量活塞式体积管标准装置标准容积进行不确定度的评定。经评定,合成标准装置标准容积相对扩展不确定度为0.010%(k=2),已经达到国际先进水平。

钟罩式气体流量标准装置不确定度分析

介绍了钟罩式气体流量标准装置的几种检定方法 ,比较了各检定方法的区别、特点及要求 ,并结合检定数据进行了不确定度分析。

超声波流量计用于原油大流量贸易计量的方案论证

超声波流量计现阶段多应用于天然气贸易计量上,对于原油贸易计量国内还没有相关标准。本文对超声波流量计用于海上平台原油大流量外输贸易计量做了方案的论证:针对海上平台空间有限的特点,对比了标准容积法、基准流量计法、标准体积管法等常用方案,采用标准体积管与基准流量计共同检定的方案,保证了计量精度,减小了流量计的尺寸和重量,降低了维护、运营成本,降低了能耗,满足国内原油贸易计量的要求。

钟罩式气体流量标准装置内部容积的测量方法

基于尺寸测量法，测量了1000L钟罩内部的分阶容积。2个接触式长度计和旋转测量臂构成弦长测量机构。将罩体沿轴向划分为若干等间距截面，以15°采样间隔测量长度计与罩体内壁的接触点到测量臂旋转中心的距离，由接触点空间坐标确定各截面的轮廓。提出一种新的面积扫描法计算各层截面面积。经与圆度误差法的测量数据对比，当采样间隔密集时（5°或15°）2种方法的测量结果比较吻合。由各层截面面积及其轴向间距，计算得到分阶容积数据表作为罩体内部容积的标定结果。

基于体积管标准装置的小流量临界流文丘里喷嘴检定方法研究

为了满足小流量临界流文丘里喷嘴的检定需求,提出了一种新的检定方法,利用高精度主动活塞式体积管作为标准装置对临界流文丘里喷嘴进行检定。由PLC控制高精度丝杆实现对体积管工作流量的精确控制,并通过比例法调节体积管流量使其与文丘里喷嘴实际流量相匹配。通过与0.2级钟罩式气体流量标准装置的检定结果进行数据比对,证明本方案是可行的。

对一类多级安全模型安全性的形式化分析

深入分析了MLS的核心思想,给出了MLS在包含多级客体的系统中的表述形式,分析了安全不变式(in-variant)在系统安全定义中的作用.为了保证模型的安全,必须验证模型的不变式满足MLS策略.为了说明不变式验证的重要性,借助Z语言和形式验证工具Z/EVES分析了一个改进的BLP模型——DBLP模型.分析表明,DBLP模型的不变式不满足MLS策略的要求,因此是不安全的.这项研究为分析各种改进BLP模型的安全性提供了理论依据和形式化规范与验证的方法.

可由用户持续发展的几何自动推理平台的推理算法

目前的几何定理证明器都不具有可持续性。提出一种结构具有一般性的知识表示和能够统一处理所有规则的推理算法,初步实现了可由用户持续发展的几何自动推理平台。该推理平台允许用户添加几何知识,如几何对象、谓词和规则,并可以综合使用多种推理算法,如前推搜索法和一部分面积法,它将更适合用于几何教学。

气体流量标准装置钟罩外径测量方法的研究

钟罩式气体流量标准装置的钟罩外径测量是几何测量法中最重要的测量参数,其不确定度分析是否准确就成为必须解决的问题。以容积为100 L的钟罩为研究对象,应用π尺法、激光跟踪法和外径千分尺法3种不同的实验方法,分别对钟罩不同截面上的外径进行了测量。对测量结果进行了比较和分析,3种测量方法引入的不确定度都在允许的范围内,由此得到3种测量方法都是正确合理的结论。通过对数据的分析,就国产的钟罩而言,相对较好的测量方法是π尺法。

断言语言支持自定义谓词的程序验证器原型

基于逻辑推理的方法进行程序验证是形式化程序验证的研究热点.目前的自动验证工具为了保证自动性,对描述程序性质的断言语言都有较多限制,导致程序的某些递归性质难以用断言语言表述.本文在一个面向指针程序、基于先前自行设计的形状图逻辑、依赖于自动定理证明工具Z3的自动程序验证原型系统上,通过在断言语言中引入自定义谓词来增强断言语言的表达能力,使得该原型系统不仅能自动验证含操作易变数据结构的程序的性质,也能自动验证一些不含指针的程序的性质.

程序求精新策略及自动验证方法研究

传统的程序求精策略无法求精至可执行程序,且存在验证的可信度低和自动化程度不高的问题。针对上述问题,提出一种较完整的程序求精策略并给出自动验证方法。使用递归定义函数技术刻画问题规约,基于Morgan精化规则程序求精至IMP程序,并使用验证条件生成器(verification condition generator,VCG)自动生成验证条件,通过Isabelle定理证明器验证IMP程序的正确性,最后利用开发平台自动生成C++可执行程序。以最长标志基因序列问题为实例进行程序求精和自动验证,检验了所提策略的有效性。该策略提高了算法程序开发的正确性,减轻了传统验证烦琐的工作量。

安全协议的形式化需求及验证

该文采用近世代数和时序逻辑的方法提出并描述了密码协议的形式化安全需求,并在AT模型的基础上加入信任和知识的非单调逻辑,建立了安全协议的计算模型。利用该计算模型对Denning_Sacco公钥协议进行了验证,发现了对此协议的重放攻击,并对协议进行了修改。

微波消解-全谱直读等离子体发射光谱法测定面包改良剂中总溴的研究

采用微波消解样品、全谱直读等离子体发射光谱法 (ICP -AES)测定面包改良剂中的溴含量。通过试验 ,优化了微波消解的条件和仪器的最佳工作参数。154.065nm波长处溴的检出限为0.015mg/L(3δ) ,线性范围为0.05～100mg/L ,样品分析结果的相对标准偏差小于5 %(n=7) ,加标回收率在93 %～105 %之间 ,样品分析结果与分光光度法相一致。该法简便、快速、灵敏、准确、线性范围宽。