-
题名以太坊智能合约定理证明中的形式化规约研究综述
被引量:1
- 1
-
-
作者
华景煜
黄达明
-
机构
南京大学计算机科学与技术系
-
出处
《信息网络安全》
CSCD
北大核心
2022年第5期11-20,共10页
-
基金
江苏省前沿引领技术基础研究专项[BK20202001]。
-
文摘
以太坊智能合约的形式化验证是目前的研究热点,在各种形式化验证方法中,定理证明方法具有误报少、可以处理大状态空间等优点。定理证明需要强大的形式化规约表达能力作为基础。文章对现有以太坊智能合约的定理证明研究中使用的形式化规约表达方法进行综述,从智能合约开发语言和区块链内生语义的建模、智能合约安全属性和功能属性的形式化规约表达、自动定理证明和交互式定理证明的选择等角度对形式化规约方法进行比较和讨论,并指出目前的困难和未来的研究方向。
-
关键词
以太坊
智能合约
形式化规约
形式化验证
定理证明
-
Keywords
Ethereum
smart contract
formal specification
formal verification
theorem proving
-
分类号
TP309
[自动化与计算机技术—计算机系统结构]
-
-
题名基于指纹识别的室内定位中的隐私保护
被引量:1
- 2
-
-
作者
张钊
华景煜
-
机构
南京大学计算机科学与技术系
-
出处
《南京信息工程大学学报(自然科学版)》
CAS
2017年第5期551-559,共9页
-
基金
国家自然科学基金(11471003
61425024)
-
文摘
基于指纹识别的定位是最流行的室内定位方法.在离线阶段,服务器测量指纹,比如来自特定空间已知位置的不同接入点(AP)的接收信号强度(RSS),测量后服务器将测量结果保存在数据库中;在线上阶段,用户同时向服务器发送他当前指纹的测量结果以及位置查询请求,服务器将在数据库中查找与测量结果最接近的指纹.虽然这种方法已经被研究了很久,但现有的工作并没有考虑2个隐私要求:供应商希望保护他们花大代价收集的指纹,用户想要对服务器保留他们的指纹测量结果,以避免泄漏位置.为了实现隐私保护,本文提出一种使用加密技术的指纹匹配方案,这个方案在加密情况下计算由用户测量的指纹与服务器存储的指纹的距离,服务器存储的指纹在这一过程中仍处于密文空间.本文证明了这个方案在进行单点定位时能够很好地保证两者的隐私要求.为了减少高昂的时间开销,本文还提出了一个基于网格划分的改进方案,以及以有限的隐私损失为代价的扩展方案.为加强安全性,最后提出了有效对抗特定攻击的对策,在这种攻击中恶意用户可以通过重复定位获得服务器存储的指纹.使用公众RSS指纹数据集的扩展实验结果显示本文方案足以在实现实时定位的同时保留定位精度.
-
关键词
基于指纹定位
室内定位
隐私保护
-
Keywords
fingerprinting-based localization
indoor localization
privacy preserving
-
分类号
O429
[理学—声学]
-
-
题名顶点P_k覆盖问题的研究综述
- 3
-
-
作者
王利民
华景煜
-
机构
南京大学计算机科学与技术系
-
出处
《南京信息工程大学学报(自然科学版)》
CAS
2017年第5期455-461,共7页
-
基金
国家自然科学基金(11471003
61425024)
-
文摘
顶点覆盖问题是经典的NP完全问题,在排序、计算机网络等现实生活中有许多的应用.近几年来,许多研究者开始探究它的推广形式——顶点P_k覆盖(VCP_k)问题,即寻找一个顶点子集,从拓扑结构图中删除后使得剩下的顶点导出的子图不包含P_k路,其中P_k是指包含k个顶点的路.本文简单介绍了VCP_k问题的应用背景,归纳了它在近似算法、精确算法、参数化算法3个方面的主要研究进展,并分析了一些主要的方法和技巧.在此基础上,对VCP_k问题及其相关问题的研究前景进行了展望.
-
关键词
顶点Pk覆盖
近似算法
精确算法
参数化算法
-
Keywords
vertex cover Pk
approximation algorithms
exact algorithms
parameter algorithms
-
分类号
TP391.7
[自动化与计算机技术—计算机应用技术]
-
-
题名史学新苗——失道寡助 得道多助
- 4
-
-
作者
华景煜
-
机构
江苏梅村高级中学高一(
-
出处
《历史学习》
2001年第6期37-37,共1页
-
-
关键词
高中教学
历史课程
历史论文
历史学习
江苏梅村高级中学
-
分类号
G633.51
[文化科学—教育学]
-