【摘 要】
：
随着智能手机的日益普及和移动网络的快速发展,移动应用越来越成为人们日常生活中不可或缺的一部分。越来越多的人们习惯于将个人信息保存于移动设备中,随之而来的是私密信息泄露问题的日益凸显。因此,如何保证移动应用中的信息在传播过程中不被泄露,成为了学术界与工业界广泛关注并普遍研究的问题。现有的保证应用程序信息安全的方法,主要是应用了权限访问控制的思想。即当一个应用程序提出信息的访问申请时,对应用程序进行权
论文部分内容阅读
随着智能手机的日益普及和移动网络的快速发展,移动应用越来越成为人们日常生活中不可或缺的一部分。越来越多的人们习惯于将个人信息保存于移动设备中,随之而来的是私密信息泄露问题的日益凸显。因此,如何保证移动应用中的信息在传播过程中不被泄露,成为了学术界与工业界广泛关注并普遍研究的问题。现有的保证应用程序信息安全的方法,主要是应用了权限访问控制的思想。即当一个应用程序提出信息的访问申请时,对应用程序进行权限验证,若验证通过则可以访问信息,若不通过则不可访问信息。该方法一定程度上保护了信息不被非法获取,但仍然不能保证被授权访问后的信息在传播和使用过程中满足安全需求。而信息流安全技术可以通过分析程序中数据传输的合法性来保证信息安全,因此可以用来解决现有的应用程序信息安全问题。在本文中,我们关注于移动应用领域,首先为每个应用程序设置权限集合,使用权限作为应用程序能否合法获取信息的依据,保证信息不被非法访问。对于已经获得访问权限的应用程序,我们使用信息流安全技术保证信息在后续传播和使用的过程中不会被泄露给攻击者。基于此思想,我们提出了一种形式化语言和一种信息流安全的逻辑规则,最后我们在Coq工具中完成了对语言和逻辑规则实现与验证。实践证明,我们提出的面向应用程序的信息流安全方法是一种可行的、有效的保证应用程序信息安全的方法。本文主要的贡献在于:（1）一种基于权限的信息流安全形式语言:该语言将应用程序抽象为函数的集合,并使用函数调用来完成应用程序之间的信息交互。与传统的串行语言不同,我们引入了权限的概念,使用权限作为信息交互过程中一个应用程序能否获取到信息的依据。此外,严格制定了该语言的操作语义,有利于推理逻辑的形成。（2）一套支持解密策略的信息流安全逻辑规则:该逻辑规则是一个安全类型系统,这些规则描述了在所提出的形式化语言中,如何传递信息流是安全的。与传统的信息流相比,加入了权限检查的内容,确保每个应用程序在获取信息过程中是安全的。此外,还加入了解密策略,让逻辑推理更加精确。（3）使用形式证明工具Coq进行实现与验证:在形式化定理证明工具Coq中对前文提出的形式化语言、语义和逻辑规则进行实现。在实现完成后,通过手机银行登录系统例子的建模与分析,验证了本文提出的针对应用程序的信息流安全方法的有效性和可行性。
其他文献
互联网给世界带来了惊喜,也带来了新的社会问题。随着技术的不断更新迭代,大数据的商业应用越来越多,数据成为了驱动新经济发展的“石油”,计算机工程师借助数据创造了丰富多彩的网络世界,企业借助数据联通了虚拟与现实商业世界。但数据所带来的社会问题也不在少数,个人信息泄漏、数据不正当竞争、网络主权维护及数据国家安全保护等成为困扰实践和理论的难题,立法正在尝试对数据进行规制,且已经陆续出台了《国家安全法》《网
随着社会信息化程度越来越高,信息安全理论与技术越来越受到人们的重视。信息安全的核心是密码理论和技术,自从密码技术出现之后,密码系统的安全强度问题受到了更为广泛的关注,而密码系统的安全强度问题可以归结为与系统相关的逻辑函数的各种性能问题,如非线性性,相关免疫性,平衡性,扩散性,稳定性等。因此研究逻辑函数的各种性能对密码系统的分析和设计具有重要的学术价值。 本文主要研究布尔函
无线通信的脆弱性本质上源于无线电磁环境的不确定性、不可操控性以及由此产生的自然与人为扰动。这些电磁环境产生的影响可以归结为在不确定的自然环境约束下,由不可操控性带来的可靠性、保密性和抗干扰等问题。无线内生安全利用无线信道具有的各点异性、随机时变性和第三方测不准特性等内生安全属性解决上述问题,是未来无线通信的新兴发展方向。然而,现有无线内生安全方案中仍然存在以下问题:（1）对于信息安全方案,多径在射
量子计算作为一种在理论上被证明了相对于经典计算有指数级加速效果的新型的计算方式,在各个领域的应用备受关注,如量子密码学、量子化学、量子生物学和量子金融等。量子计算当前正处于中等规模带噪声量子器件时期,这个时期的量子线路可以实现约50-100个量子比特的量子计算,量子计算优越性已经被证明。然而,这个时期的量子比特数有限且噪声较大,这给量子计算的相关算法和方案实现造成了极大的阻碍。针对当前量子比特数有
随着互联网、5G技术、云仓储等高新技术的发展,数字化图像已经成为各行各业不可或缺的一部分,为了确保图像信息的安全传输,对图像加密技术的研究成为了信息安全领域的一项重要任务。数字图像具有像素间关联性强、冗余程度高等特点,传统的图像加密技术已经满足不了数字图像的加密需求。混沌系统和DNA编码则因为其优良的特性,刚好能应用于图像加密领域,可以很好地解决数字图像的加密问题。基于此,针对现阶段图像加密的发展
环保密交易是密码货币系统中广泛使用的隐私保护技术,能够做到同时保护交易中的付款者、收款者和交易数额。隐形地址是环保密交易的核心组件之一,能够隐藏交易与交易之间、交易与用户之间的链接关系。然而,广泛使用的隐形地址方案存在两个主要的不足:（1）单个派生私钥的泄露产生的危害会扩散到整个主私钥;（2）缺乏抗量子安全性。为了解决这两个问题,我们提出用抗量子安全的密钥隔离和隐私保护的公开公钥派生签名方案,并在
目的:探究国内外儿童青少年近视的研究现状、热点和未来的发展趋势，为该领域深入研究提供借鉴和参考。方法:以中国知网（CNKI）和Web of Science（WOS）为数据源，收集2003-01-01/2022-12-31儿童青少年近视研究领域的文献，使用VOSviewer进行发文量、作者、发文机构和期刊分析；使用CiteSpace进行关键词共现、关键词聚类、关键词时间线图谱和关键词突现分析。结果:
目的：观察雷火灸治疗青少年近视的临床疗效。方法：选取2018年1月—2021年4月就诊于雅安市第三人民医院的青少年近视患者30例（近视眼数50只）,给予雷火灸治疗，刺激穴位有眼部（阳白、四白、太阳、颧髎、鱼腰、丝竹空、瞳子髎、印堂）、耳部（肝、脾、肾、目2、眼）及手部（合谷）诸穴，经治30 d,观察临床疗效。结果：临床总有效率为76.7%（23/30）。结论：雷火灸治疗青少年近视，临床效果满意。
＜正＞“二十四节气”文化是中国古代劳动人民在长期与自然交往的过程中逐步摸索、积累起来的一套时间知识体系和社会实践经验总结。它融合了天文、气象、自然界动植物的变化等多方面的科学文化，并衍生出丰富的民俗、饮食、文学艺术等多方面文化内涵。我园依托省级课题《二十四节气教育资源在幼儿园园本课程中的实践研究》，把园所附近的三角洲湿地公园作为幼儿园的特色资源，引导孩子进行节气观察，自然体验，同时进行简单的节气农
目的：研究针刺治疗后肩周炎患者的临床疗效和生存质量改善情况。方法：严格按照纳入排除标准选择2022年3月—2023年3月收治的80例肩周炎患者进行研究，按照等比例随机数字表法分为2组，对照组40例采用口服药物+功能锻炼治疗，研究组40例采用经络别通法针刺治疗，治疗1个疗程后观察比较2组临床疗效、肩关节功能、日常生活能力、炎症因子水平以及疼痛恢复。结果：研究组治疗总有效率97.50%显著高于对照组7