以太坊智能合约定理证明中的形式化规约研究综述

以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向。

基于指纹识别的室内定位中的隐私保护

基于指纹识别的定位是最流行的室内定位方法.在离线阶段,服务器测量指纹,比如来自特定空间已知位置的不同接入点(AP)的接收信号强度(RSS),测量后服务器将测量结果保存在数据库中;在线上阶段,用户同时向服务器发送他当前指纹的测量结果以及位置查询请求,服务器将在数据库中查找与测量结果最接近的指纹.虽然这种方法已经被研究了很久,但现有的工作并没有考虑2个隐私要求:供应商希望保护他们花大代价收集的指纹,用户想要对服务器保留他们的指纹测量结果,以避免泄漏位置.为了实现隐私保护,本文提出一种使用加密技术的指纹匹配方案,这个方案在加密情况下计算由用户测量的指纹与服务器存储的指纹的距离,服务器存储的指纹在这一过程中仍处于密文空间.本文证明了这个方案在进行单点定位时能够很好地保证两者的隐私要求.为了减少高昂的时间开销,本文还提出了一个基于网格划分的改进方案,以及以有限的隐私损失为代价的扩展方案.为加强安全性,最后提出了有效对抗特定攻击的对策,在这种攻击中恶意用户可以通过重复定位获得服务器存储的指纹.使用公众RSS指纹数据集的扩展实验结果显示本文方案足以在实现实时定位的同时保留定位精度.

顶点P_k覆盖问题的研究综述

顶点覆盖问题是经典的NP完全问题,在排序、计算机网络等现实生活中有许多的应用.近几年来,许多研究者开始探究它的推广形式——顶点P_k覆盖(VCP_k)问题,即寻找一个顶点子集,从拓扑结构图中删除后使得剩下的顶点导出的子图不包含P_k路,其中P_k是指包含k个顶点的路.本文简单介绍了VCP_k问题的应用背景,归纳了它在近似算法、精确算法、参数化算法3个方面的主要研究进展,并分析了一些主要的方法和技巧.在此基础上,对VCP_k问题及其相关问题的研究前景进行了展望.