Convergence of IT and SCADA: Associated Security Threats and Vulnerabilities
随着许多行业转向集中控制的信息系统以进行监视和控制，越来越重视诸如监督控制和数据采集工业系统（SCADA）的技术。这种对集成和互操作性的关注为安全人员和组织管理层带来了许多挑战。因此，在一个组织内，通过适当的计划和框架来确保其SCADA架构的保护和安全性，从而实现这一新方向变得至关重要。明确了解相关威胁和脆弱性对于采取/制定适当的政策和框架至关重要。为此，在这项研究中，我们识别和分析相关的SCADA安全威胁和漏洞，并提出了一个简单的方案来对其进行分类，以便更好地理解。
2020-05-08 cs.CR
Security Analysis of Vendor Implementations of the OPC UA Protocol for Industrial Control Systems
OPC UA协议是即将在欧洲建立工业4.0流程的事实标准，也是少数几个承诺安全功能以防止攻击者操纵和破坏关键基础设施的工业协议之一。尽管该协议非常重要，但到目前为止，产品供应商、实现该标准的库和最终用户在采用OPC UA安全功能方面面临的挑战还没有得到调查。在这项工作中，我们系统地调查了48个公开的工件组成的产品和库的OPC UA和显示，38出的48个工件有一个（或多个）安全问题。特别是，我们表明，7 OPC UA文物不支持协议的安全功能。此外，31个部分具有OPC UA安全性的工件依赖于不完整的库，并带有误导性的说明。因此，依赖这些产品和库将导致OPC UA安全功能的脆弱实现。为了验证我们的分析，我们设计，实施和演示攻击，攻击者可以窃取受害者之间交换的凭证，窃听进程信息，通过传感器值和执行器命令操纵物理过程，并防止检测到异常。
2021-11-08 cs.CR
Coinbugs: Enumerating Common Blockchain Implementation-Level Vulnerabilities
大量的工作一直致力于调查和系统化以太坊智能合约安全漏洞类。然而，在调查比特币存在的第一个十年期间发现的基本PoW区块链节点实现中常见的实现级安全漏洞时，文献中存在差距。本文试图填补这一空白。特别是，如果通过验证和生成新块来参与网络的软件是从头开始开发的，那么WCGW - What Could Go Wrong？列出了10大错误类型类别，并为每个类别链接了已知的示例。中本聪论文所设计的区块链令人兴奋，并引入了几个安全研究人员感兴趣的新颖错误类。本文针对的是安全测试人员，旨在从区块链安全审查和区块链开发人员开始，作为常见陷阱的参考。
2021-04-13 cs.CR
SoK: An Analysis of Protocol Design: Avoiding Traps for Implementation and Deployment
今天的互联网使用多种不同的协议。虽然其中一些协议是首先实施和使用并随后记录的，但其他协议是首先指定然后实施的。无论协议是如何形成的，它们的定义都可能包含导致不安全的实现或部署的陷阱。一个典型的例子是协议规范中的认证要求不够严格。由此产生的错误配置，即，不启用强身份验证是Internet安全事件的常见根本原因。事实上，互联网协议通常在设计时没有考虑到安全性，这导致了大量的错误配置陷阱。虽然这种情况正在慢慢改变，但严格的安全考虑可能会产生类似的不良影响。由于复杂的实施和不充分的文档，安全功能可能仍然未使用，使部署容易受到攻击。在本文中，我们提供了一个系统的安全陷阱中发现的常见的互联网协议。通过将协议分为四类，我们确定了导致常见安全陷阱的主要因素。这些见解以及对以最终用户为中心的可用性和默认安全性的观察，然后用于获得改进现有协议和设计新协议的建议-而不会为运营商，实施者和用户设置此类安全敏感陷阱。
2016-10-18 cs.CR
Algorithmic Security is Insufficient: A Comprehensive Survey on Implementation Attacks Haunting Post-Quantum Security
本综述探讨了后量子密码（PQC）算法面临的侧信道攻击（SCA）威胁及其对策，指出仅靠算法安全性不足以应对实现攻击，并提供了PQC研究的最新进展与未来愿景。
2023-05-22 cs.CR
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
MPC-in-the-Head（MitH）是一个通用的框架，它允许从安全多方计算（MPC）协议构造有效的一般NP关系的零知识协议。在本文中，我们给出了这种转换的第一个机器检查的实现。我们从MitH的EasyCrypt形式化开始，它保留了MitH的模块化结构，并且可以用满足标准安全概念的任意MPC协议来实例化，这使我们能够利用现有的基于机器检查的秘密共享的MPC协议开发。在EasyCrypt中证明了ZK协议的安全性和正确性。使用最近开发的代码提取机制EasyCrypt，我们合成了一个正式验证的协议的实现，我们基准测试，以获得与我们的形式化选择和代码提取机制相关的开销的指示。
2021-05-19 cs.CR
Finding Security Vulnerabilities in IoT Cryptographic Protocol and Concurrent Implementations
物联网（IoT）由大量通过网络连接的设备组成，这些设备交换大量数据，从而带来新的安全，隐私和信任问题。解决这些问题的一种方法是使用物联网协议的轻量级加密算法来确保数据机密性。然而，这种协议的设计和实现是一项容易出错的任务;实现中的缺陷可能导致破坏性的安全漏洞。在这里，我们提出了一种新的验证方法命名为加密BMC和Fuzzing（EBF），它结合了有界模型检验（BMC）和Fuzzing技术来检查安全漏洞，出现并发实现的并行图形协议，其中包括数据竞争，线程泄漏，算术溢出，内存安全。EBF使用POSIX线程将IoT协议建模为客户端和服务器，从而模拟两个实体的通信。它还采用静态和动态验证，以涵盖系统的状态空间详尽。我们评估EBF对三个基准。首先，我们使用SV-COMP的并发基准测试，并表明它在错误发现方面优于其他最先进的工具，如ESBMC，AFL，Lazy-CSeq和TSAN。其次，我们评估了一个名为WolfMQTT的开源实现。它是一个使用WolfSSL库的MQTT客户端实现。我们发现，\tool检测数据竞争的错误，其他方法是无法找到的。第三，为了证明EBF的有效性，我们复制了OpenSSL和CyaSSL（最近的WolfSSL）库中的一些已知漏洞。EBF可以在最短的时间内检测到错误。
2021-04-27 cs.CR
A Quic(k) Security Overview: A Literature Research on Implemented Security Recommendations
本研究通过评估RFC9000的10项安全考虑对13个生产级QUIC实现进行文献分析，发现复杂标准导致生态系统碎片化，且现有实现安全性尚不成熟。
2023-06-30 cs.CR
Gamifying Education and Research on ICS Security: Design, Implementation and Results of S3
在这项工作中，我们认为有关安全的工业控制系统（ICS）的ICS安全教育和研究的背景下，以学术界和工业界的挑战。我们建议通过游戏化的攻击训练和对策评估来应对这些挑战。我们在（据我们所知）第一个针对ICS安全的捕获旗帜（CTF）事件（称为SWaT安全摊牌（S3））的背景下测试了我们提出的ICS安全游戏化想法。六个团队在利用ICS测试平台的安全竞赛中充当攻击者，几个学术防御系统试图检测正在进行的攻击。活动分两个阶段进行。在线阶段（危险风格的CTF）作为培训课程。现场阶段的结构是一个攻击-防御CTF。我们担任裁判，根据我们内部开发的基于多种因素（包括真实的攻击者模型）的评分系统为攻击者团队分配分数。最后，我们对S3进行了评估和讨论，包括从S3每个阶段收集的数据中得出的统计数据。
2017-02-10 cs.CR
Testing side-channel security of cryptographic implementations against future microarchitectures
该研究针对未来微架构优化对密码实现的侧信道安全影响评估缺失问题，开发了泄漏模型描述语言LmSpec与自动测试框架LmTest，经实证发现18种待落地优化会导致现有25种密码实现均存在密钥相关泄漏。
2024-02-01 cs.CR
Analysing the Security of Google's implementation of OpenID Connect
数以百万计的用户经常使用他们的Google帐户登录支持Google OpenID Connect服务的依赖方（RP）网站。OpenID Connect是一种新标准化的单点登录协议，它在OAuth 2.0协议之上构建了一个身份层，该协议本身已被广泛采用以支持身份管理服务。它为OAuth 2.0系统添加了身份管理功能，并允许RP获得有关最终用户真实性的保证。许多作者分析了OAuth 2.0协议的安全性，但OpenID Connect在实践中是否安全仍然是一个悬而未决的问题。我们报告的大规模的实际研究谷歌的实施OpenID连接，涉及法医检查103 RP网站，支持其使用的登录。我们的研究揭示了许多类型的严重漏洞，所有这些漏洞都允许攻击者以受害者用户身份登录RP网站。进一步的研究表明，这些漏洞是由Google的OpenID Connect服务设计和RP开发人员做出的牺牲安全性以简化实现的设计决策相结合造成的。我们还为RP和OP提供了实用的建议，以帮助提高真实世界OpenID Connect系统的安全性。
2015-08-07 cs.CR
On The Security Evaluation of Partial Password Implementations
部分密码是一种广泛使用的基于密码的身份验证模式，特别是在金融领域。它基于一个挑战-响应协议，在每次登录尝试时，一个挑战请求字符从一个预先共享的秘密随机选择的位置呈现给用户。这种模式可以被看作是一种廉价的方式，可以防止安装在用户设备上的恶意软件或键盘记录器在单步的学习完整的密码。尽管这一机制被广泛采用，特别是许多英国银行，但公开文献中的材料有限。诸如该方案的安全性如何随用于形成挑战的采样方法而变化或现有服务器端实现是什么之类的问题没有得到解决。在本文中，我们研究的问题，如这种机制的安全性如何变化的挑战-响应对的数量可供攻击者根据不同的方式生成的挑战。此外，我们还讨论了可能的服务器端实现，因为信息安全专家在不同的在线论坛中“非正式地”列出了这些实现。据我们所知，没有正式的学术文献在这个方向上，本文的目的之一是激励其他研究人员研究这个问题。
2016-12-31 cs.CR
Independent Co-Assurance using the Safety-Security Assurance Framework (SSAF): A Bayesian Belief Network Implementation for IEC 61508 and Common Criteria
安全保障框架适用于两个标准IEC 61508和通用标准- ISO 15408
2020-10-13 cs.CR cs.SE
An Improved FPGA Implementation of the Modified Hybrid Hiding Encryption Algorithm (MHHEA) for Data Communication Security
混合隐藏加密算法，顾名思义，包含隐写术和密码学的概念。本文提出了一种改进的微结构现场可编程门阵列（FPGA）实现算法。这种设计克服了先前设计的微架构的观察到的限制。这些观察到的局限性是：没有利用并行比特替换的可能性，以及输入明文被串行加密的事实，这导致吞吐量与所使用的秘密密钥的性质之间的依赖性。这种依赖性可以被一些人视为所实现的微架构的安全性中的漏洞。所提出的修改后的微架构构造使用五个基本模块。这些模块是：消息缓存、消息对齐模块、密钥缓存、比较器，最后是加密模块。在这项工作中，我们提供了全面的模拟和实施结果。这些是：时序图，实施后的时序和路由报告，最后是平面图。此外，与其他FPGA实现的详细比较，并进行了讨论。
2007-10-25 cs.CR
An Automated Security Analysis Framework and Implementation for Cloud
云服务提供商为其客户提供按需且经济高效的服务、可扩展计算和网络基础设施。企业将其服务迁移到云以利用云计算的好处，例如消除其计算需求的资本支出。云中存在安全漏洞和威胁。许多研究已经提出了使用图形安全模型（GSM）和安全度量来分析云安全。此外，它已经被广泛研究，为云的安全性找到适当的防御策略。移动目标防御（MTD）技术可以利用云的弹性特性改变攻击面，迷惑攻击者。以前的大部分工作，将MTD到GSM的理论和性能进行了评估的基础上的模拟。在本文中，我们实现了上述框架，并设计，实现和测试一个云安全评估工具在一个真正的云平台名为UniteCloud。我们的安全解决方案可以（1）实时监控云计算，（2）自动化安全建模和分析，并通过Web应用程序使用图形用户界面可视化GSM，以及（3）在真实的云基础设施上部署三种MTD技术，包括多样性，冗余和洗牌。我们使用API分析了自动化过程，并展示了在UniteCloud上自动部署所有三种MTD技术的实用性和可行性。
2019-04-03 cs.CR
Design and Implementation of A Network Security Management System
近年来出现的网络蠕虫和攻击具有分布性，可以在很短的时间内在全球范围内传播。迫切需要跨网络的安全管理，共同防御网络范围内的攻击，提高安全管理效率。提出了一种分层分布式网络安全管理系统（HD-NSMS），它可以集中管理跨网络的安全。首先从宏观和微观两个方面对系统进行了描述;然后讨论了构建HD-NSMS时的三个关键问题：设备模型、告警机制和应急响应机制;最后描述了HD-NSMS的实现。本文的工作来源于一个实际的网络安全管理系统，对网络安全管理系统的实现具有一定的参考价值。
2016-09-03 cs.CR cs.NI
Security Problems with Improper Implementations of Improved FEA-M
本文报告了FEA-M（多媒体快速加密算法）的一个改进版本的不正确实现的安全问题。据发现，实现依赖的差分选择明文攻击或其选择密文对应物可以揭示的秘密密钥的密码系统，如果所涉及的（伪）随机过程可以被篡改（例如，通过公共时间服务）。实现相关差分攻击在复杂度上是非常有效的，并且仅需要$O(n^2)$选择明文或密文比特。此外，本文还指出了会话密钥选择中的一个小安全问题。在密码系统的实际实现中，应该小心地避免这些安全问题，或者密码系统必须进一步增强以在这种弱实现下工作。
2006-06-25 cs.CR cs.MM
SoK: What don't we know? Understanding Security Vulnerabilities in SNARKs
本文针对现有SNARK研究重理论安全证明、轻实际实现安全的问题，构建系统与威胁模型，分析141个真实漏洞并给出分类体系，评估现有防御机制并提出安全增强建议，助力SNARK系统更可靠落地。
2024-07-11 cs.CR
Efficient Hardware Implementation of Constant Time Sampling for HQC
针对NIST后量子密码候选方案HQC的新型抗侧信道采样算法，提出跨层优化的高效硬件实现方案，在Xilinx Artix 7 FPGA上验证显示延迟大幅降低且资源占用更少。
2025-06-17 cs.CR
A Novel Data Encryption Algorithm Design and Implementation in Information Security Scope
今天，信息的保护，确保安全性和在需要的情况下无损召回是非常重要的，它被视为该领域的主要威胁。信息安全通过隐藏可用数据、加密、保存、传输和共享而成为可能。在这一点上，密码学主题出现。密码学被称为密码学，包括按照一定的技术对不同的文本进行加密，并在安全的环境中将这些信息传输给接收者。在本研究中，在信息安全范畴内，发展了一种新颖的数据加密算法。设计了基于“单字符重定位”技术的算法。在算法的创建过程中，还利用了来自凯撒的加密算法、多字母表算法和Enigma。研究的目的是以安全的方式存储所写的文本，从而确保信息安全，并根据要求进行解密。在这项研究中，开发了一种非常难以解密的算法，当考虑使用密码字母表的数量时，这显然是新兴的。本研究可望对信息安全领域有所贡献。
2019-02-09 cs.CR
Trusted Enforcement of Application-specific Security Policies
虽然二十多年来一直存在用于将安全策略集成到操作系统（OS）中的方法，但是应用通常使用需要具有应用特定语义的单独安全策略的更高抽象的对象。由于操作系统支持不足，当前用于实施应用级策略的方法通常导致大型且复杂的可信计算基础，从而难以实现防篡改性和正确性。为了缓解这个问题，我们提出了应用程序级的策略执行架构AppSPealing和一个C++框架，其实现。可配置的框架使开发人员能够平衡强制执行的严格性和不同实现方案所带来的成本，从而轻松地根据各个应用程序的要求定制AppSPSecurity实现。我们特别认为，基于硬件的可信执行环境提供了政策保护和执行的有效性和效率之间的最佳平衡。这一说法得到了基于电子病历系统的实际评价的证实。
2021-05-05 cs.CR
Do Skill Descriptions Tell the Truth? Detecting Undisclosed Security Behaviors in Code-Backed LLM Skills
Skill Security Team（技能安全团队）
本文研究LLM生态系统中程序性技能描述与实现之间的不一致，通过构建安全属性分类法和SKILLSCOPE工具，发现9.4%的技能存在安全风险，工具在识别不一致时达到84.8%的精度和96.5%的召回率。
2026-05-13 cs.CR
Directed Security Policies: A Stateful Network Implementation
大型系统通常是互连的。安全策略描述网络实体之间的通信关系。安全策略定义规则，例如A可以连接到B，这会产生一个有向图。然而，该策略通常在网络中例如通过防火墙来实现，使得A可以建立到B的连接，并且允许属于所建立的连接的所有分组。这种有状态的实现通常是网络功能所必需的，但它引入了从B到A的回流，这可能与安全策略相矛盾。我们推导出一个策略及其有状态实现的合规标准。特别是，我们提供了一个标准来验证在线性时间内没有副作用。提出了自动构造安全策略规则的有状态实现的算法，缩小了形式化与实际实现之间的差距。该解决方案可扩展到大型网络，这一点已被一个大型现实案例研究所证实。它的正确性由Isabelle/HOL定理证明器保证。
2014-05-06 cs.CR cs.LO
A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
本文提出一种直接在协议实现层面进行强安全属性模块化验证的通用方法，利用先进验证逻辑和工具支持多种语言，并在Go和C语言的原型实现中验证了多个协议的内存安全性和安全性。
2023-09-10 cs.CR cs.PL
Security of the DNS Protocol - Implementation and Weaknesses Analyses of DNSSEC
今天，互联网提供了许多关键的应用。因此，对于互联网服务提供商来说，确保操作的可追溯性和安全的数据交换变得非常重要。由于所有这些通信都基于使用域名系统（DNS）协议，因此有必要考虑通过提出该协议的安全版本来增强和保护它，该协议可以纠正DNS协议的全部或部分弱点和漏洞。在这种情况下，DNSsec由IETF创建，以确保DNS数据的完整性和对此类数据源的身份验证。DNSsec是基于公钥密码技术提供不同的安全服务。在本文中，我们将首先介绍DNS协议及其弱点。之后，我们将有兴趣研究DNSsec的实现和数据交换，并对其弱点进行深入分析。
2012-07-30 cs.CR
Statistical Analysis of Privacy and Anonymity Guarantees in Randomized Security Protocol Implementations
UC Berkeley（加州大学伯克利分校）
安全协议通常使用随机化来实现概率非确定性。这种非确定性反过来又用于混淆可观察值对秘密数据的依赖性。由于安全协议的正确性非常重要，安全协议的形式化分析在文献中得到了广泛的研究。随机安全协议也被分析使用形式化技术，如进程演算和概率模型检验。在本文中，我们考虑的问题，验证实现的随机化协议。与以前的方法，把协议作为一个白盒，我们的方法试图验证一个实现提供了一个黑盒。我们的目标是通过统计技术推断安全协议提供的保密性保证。我们学习的概率依赖的可观察的输出秘密输入使用贝叶斯网络。然后，这被用来近似秘密的泄漏。为了评估我们的统计方法的准确性，我们比较了我们的技术与概率模型检验技术的两个例子：人群协议和餐饮密码学家的协议。
2009-06-27 cs.CR cs.LG
Integrating Remote Attestation with Transport Layer Security
英特尔®软件防护扩展（英特尔® SGX）是一种很有前途的技术，可在不受信任的环境中安全地处理信息。英特尔SGX的一个重要方面是能够执行远程认证以评估端点的可信度。最终，远程证明将产生经证明的安全信道以将秘密提供给飞地。我们将英特尔SGX远程认证与标准传输层安全（TLS）连接的建立无缝结合。远程证明在连接设置期间执行。为了实现这一点，我们既不改变TLS协议，也不修改现有的协议实现。我们有三个广泛使用的开源TLS库的原型实现：OpenSSL，SSL和mbedTLS。我们描述了将经过认证的TLS端点无缝绑定到英特尔SGX安全区的要求、设计和实施细节。
2019-07-26 cs.CR
Model of solutions for data security in Cloud Computing
本文的目的是开发一个模型，以确保数据存储在云中。基于商业环境中出现的情况的模型。该模型还包括个人参与者及其数据操作。该模型的实现是使用UML传输。该模型分为7个模块。每个模块都从数据安全的条款中显而易见，并描述了处理数据时的特定情况。基于这个模型，可以将云计算的实施转换为企业环境中的数据安全。
2013-07-14 cs.CR
Performance Evaluation of Security Protocols
我们提出了一个比较性能评估的安全协议。我们的方法的新颖之处在于使用多项式数学模型，捕获的性能类的加密算法，而不是单独捕获每个算法的性能，在其他论文中使用的方法。使用这种模型的一个主要优点是它不需要特定于实现的信息，因为决策是基于比较协议的估计性能，而不是实际评估它们。通过比较评估1000个自动生成的安全协议的性能对其实际实现的性能，该方法是有效的。
2009-10-20 cs.CR
Towards Implementation of Robust and Low-Cost Security Primitives for Resource-Constrained IoT Devices
近年来，由于全球化的趋势，系统集成商不得不比以往任何时候都更多地处理集成电路（IC）/知识产权（IP）假冒问题。这些伪造的硬件问题已经推动了对更安全的芯片认证的需求。来自物理源的高熵随机数是安全系统中认证和加密过程的关键组成部分[6]。安全加密依赖于用于生成密钥的真正随机数的源，并且需要片上随机数生成器来实现足够的安全性。此外，物联网（IoT）采用了大量基于硬件的安全和预防解决方案，以便以资源有效的方式安全地交换数据。在这项工作中，我们已经开发了几种基于硬件的随机函数的方法，以解决问题并增强IC的安全性和信任度：一种新颖的基于DRAM的固有物理不可克隆函数（PUF）[13]，用于系统级安全性和认证以及分析各种环境条件的影响，特别是硅老化;基于DRAM剩磁的真随机数生成（TRNG），以产生具有非常低开销的随机序列;用于产生无限数量的随机比特的基于有效电源噪声的TRNG模型，其已经被评估为成本有效的技术;物联网（IoT）环境的架构和硬件安全解决方案。由于物联网设备受到严重的资源限制，我们提出的设计可以以高效和低成本的方式减轻建立可信和安全性的担忧。
2018-06-14 cs.CR
Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack: A Pledge for Formal Methods in the Field of Implementation Security
在我们在PROOFS 2013上的论文中，我们正式研究了一些已知的对策，以保护CRT-RSA免受BellCoRe故障注入攻击。然而，我们留下了警惕的对策和Coron等人声称的修复版本作为未来的工作，因为我们的工具的算术框架不够强大。在本文中，我们弥合这一差距，然后使用相同的方法来正式研究这两个版本的对策。我们得到了令人惊讶的结果，我们相信这表明了形式化分析在实现安全领域的重要性。事实上，最初版本的警惕的对策实际上是坏了，但没有科伦等人认为的那么多。因此，他们提出的修复版本可以简化。它实际上可以进一步简化，因为九个模块验证中的两个恰好是不必要的。幸运的是，我们可以正式证明简化的修复版本可以抵抗BellCoRe攻击，这被对策的作者自己认为是一个“具有挑战性的问题”。
2014-05-23 cs.CR
Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)
我们提供了一个由工具和元定理组成的安全协议端到端验证框架，它弥合了自动化协议验证和代码级证明之间的差距。我们自动将Tamarin协议模型转换为一组用分离逻辑表示的I/O规范。每个这样的规范描述协议角色的预期I/O行为，然后验证角色的实现。我们的可靠性结果保证了验证的实现继承了Tamarin模型证明的所有安全（跟踪）属性。因此，我们的框架使我们能够利用Tamarin先前的大量验证工作来验证新的和现有的实现。使用任何分离逻辑代码验证器的可能性提供了关于目标语言的灵活性。为了验证我们的方法并证明它可以扩展到现实世界的协议，我们验证了WireGuard VPN密钥交换协议的官方Go实现的实质性部分。
2022-12-08 cs.CR cs.PL
LpiCT: A logic security analysis framework for protocols
针对pi演算难以及时发现密码协议设计与实现逻辑缺陷的问题，本文融合逻辑规则、二叉树和KMP算法扩展pi演算，提出LpiCT框架，并通过TLS1.3验证其有效性。
2023-11-01 cs.CR cs.LO
Power Side Channels in Security ICs: Hardware Countermeasures
功率侧信道攻击是一种非常有效的密码分析技术，它可以通过监测功耗来推断安全IC的密钥。自90年代后期出现实际攻击以来，它们一直是许多配备密码的设备的主要威胁，包括灵巧卡，加密FPGA设计和移动电话。密码设备的设计者和制造商已经相应地开发了用于保护的各种对策。攻击方法也不断发展，以对抗抵抗性实现。本文回顾了基本的功耗分析攻击技术，并研究了各种硬件设计缓解措施。其目的是突出暴露的漏洞，在基于硬件的对策，为未来更安全的实施。
2016-05-02 cs.CR
Finding Security Vulnerabilities in Network Protocol Implementations
网络协议的实现在访问内存区域和处理算术运算时，往往容易出现由于开发人员的错误而导致的漏洞。寻找实用的方法来检查网络协议实现的安全性已被证明是一个具有挑战性的问题。其主要原因是协议软件状态空间太大，难以探索。在这里，我们提出了一种新的验证方法，结合模糊与符号执行，以验证复杂的属性在网络协议实现。我们使用模糊的初步探索的网络协议，而符号执行探索的程序路径和协议状态，这是发现模糊。从这个组合，我们自动生成高覆盖率的测试输入数据包的网络协议的实施。我们调查了基于模糊和符号执行的各种方法，以了解这些技术如何有效地结合起来，然后选择一个合适的工具来进一步开发我们的模型在我们的初步评估中，我们使用ESBMC，Map2Check和KLEE作为软件验证器和SPIKE作为模糊器，以检查它们是否适合验证我们的网络协议实现。我们的实验结果表明，ESBMC可以在我们的验证框架\textit{FuSeBMC}中进一步开发，以有效地检测网络协议实现中复杂的安全漏洞。
2020-01-27 cs.CR cs.NI
Enterprise API Security and GDPR Compliance: Design and Implementation Perspective
随着企业级业务发展的不断进步，对新应用和服务的需求是压倒性的。为了开发和交付这些应用程序和服务，企业业务依赖于应用程序编程接口（API）。从本质上讲，API是一把双刃剑。一方面，API通过共享价值和实用性提供了扩展业务的便利，但另一方面，它带来了安全和隐私问题。由于应用程序通常使用API来检索重要数据，因此确保有效的访问控制和安全机制到位，并且数据不会落入坏人之手是非常重要的。在本文中，我们讨论了企业API安全的现状以及机器学习（ML）在API安全中的作用。我们还讨论了通用数据保护条例（GDPR）合规性及其对API安全性的影响。
2019-09-17 cs.CR cs.NI
Desiging a logical security framework for e-commerce system based on soa
信息技术的迅速发展也改变了现有的市场，使它们从有形市场转变为电子市场（电子商业）。随着电子商业的发展，企业必须找到一种更安全的方法来实现电子商业并维护其逻辑安全。SOA是满足这些需求的最佳技术之一。SOA具有易于使用、灵活和可回收的优点。SOA的这些优点也使得消息篡改和非授权访问变得容易。这使得电子商业的安全技术实现在其他工程学科中非常困难。本文讨论了在电子商业中使用SOA的重要性，并指出了现有电子商业平台安全分析中存在的缺陷。在发现缺陷的基础上，本文还提出了SOA支持的电子商业系统逻辑安全框架的实现设计。
2014-07-09 cs.CR
An Outline of Security in Wireless Sensor Networks: Threats, Countermeasures and Implementations
随着无线传感器网络（WSNs）规模的不断扩大，对网络中数据流安全的需求也在不断增加。这些传感器网络允许易于应用和灵活的安装，使它们能够用于许多应用。由于这些属性，它们面临着不同的信息安全威胁。跨网络流动的数据的安全性为研究人员提供了一个有趣和有趣的研究潜力。这些网络的设计，以确保数据的保护面临着有限的功率和处理资源的约束。我们提供了无线传感器网络安全的基础知识，以帮助研究人员和工程师更好地了解这一应用领域。在本章中，我们将提供信息安全的基础知识，特别强调无线传感器网络。本章还将概述这些网络中的信息安全要求。分析了无线传感器网络中数据安全面临的威胁，并提出了相应的对策。
2013-01-14 cs.CR cs.NI
The security of the Coordicide: the implementation and analysis of possible attack vectors
本文的目标是研究和分析Iota网络2.0版本协议可能的攻击向量。在这项工作中，研究了分布式账本技术的现有攻击向量，并讨论了它们对Iota 2.0协议的适用性。在运行完整节点软件版本的节点网络中，提出并分析了一种针对诚实参与者写入账本的能力的特定攻击。
2022-05-25 cs.CR cs.DC
The Passwordless Authentication with Passkey Technology from an Implementation Perspective
本文从实现视角分析基于 Passkey 的无密码认证技术，对比 TOTP 机制，展示其在防泄露、防钓鱼和抗暴力破解方面的安全优势，并探讨实际集成与部署的可行性。
2025-08-16 cs.CR
WPSE: Fortifying Web Protocols via Browser-Side Security Monitoring
我们提出了WPSE，浏览器端的Web协议的安全监视器，旨在确保符合预期的协议流，以及消息的机密性和完整性。我们正式证明，WPSE是足够的表达，以保护Web应用程序从广泛的协议实现错误和Web攻击。我们讨论了具体的攻击，可以防止WPSE OAuth 2.0和SAML 2.0，包括一个新的攻击谷歌实现的SAML 2.0，我们发现通过形式化的协议规范WPSE。此外，我们使用WPSE在野外对OAuth 2.0进行了广泛的实验评估。在90个测试网站中，我们发现了55个网站（61.1%）的安全漏洞，包括Facebook Pixel等跟踪库引入的新的关键漏洞，所有这些漏洞都可以通过WPSE修复。最后，我们发现WPSE在83个网站（92.2%）上可以正常工作，其中7个兼容性问题是由偏离OAuth 2.0规范的自定义实现引起的，其中一个引入了严重漏洞。
2018-06-24 cs.CR
Formal-Guided Fuzz Testing: Targeting Security Assurance from Specification to Implementation for 5G and Beyond
本研究提出形式化引导的模糊测试方法，结合形式化验证与模糊测试的优势，分层检测5G协议到软件栈的漏洞，在srsRAN平台发现61个漏洞，将计算成本从指数增长降为线性增长。
2023-07-20 cs.CR
DT-SIM: Property-Based Testing for MPC Security
针对MPC协议安全检测形式化方法难度高、缺自动化工具的问题，提出基于属性的灰盒测试方法，借助概率编程与统计推断，可高效检测MPC比特级实现的安全漏洞。
2024-03-12 cs.CR
PrettyCat: Adaptive guarantee-controlled software partitioning of security protocols
一个简单的错误就可能导致当今大型单片软件的所有安全性受到全面损害。软件的分区可以帮助简化代码审查和验证，而软件组件的隔离执行可以限制不正确实现的影响。然而，现有的应用程序分区技术太昂贵，太不精确，或涉及不安全的手动步骤。目前还没有一种自动而安全的方法来将安全协议分解为基于组件的系统。我们提出了一种方法和工具集，自动隔离安全相关的软件到一个无限数量的分区，根据所需的安全保证部署的加密构建块。由于分区会带来通信开销，我们提供了一系列合理的性能优化。此外，通过将我们的方法应用于安全消息传递协议OTR，我们证明了它的适用性，并实现了可信计算基础的显着减少。与单片实现相比，只有29%的分区协议需要机密性保证，其进程开销与常见的沙箱技术相当。
2017-06-15 cs.CR
Harzer Roller: Linker-Based Instrumentation for Enhanced Embedded Security Testing
由于物联网的兴起，有许多新的芯片和平台可供业余爱好者和工业界使用，以构建智能设备。这些新平台的SDK通常包括包含无线协议实现、加密实现或其他库函数的闭源二进制文件，这些文件在平台上的所有用户代码中共享。利用这样的库漏洞对给定的平台有很大的影响。然而，由于这些平台通常是现成的，像JTAG这样的经典调试基础设施往往是不可用的。在本文中，我们提出了一种方法，称为Harzer辊，以提高资源受限的设备上的嵌入式固件安全测试。使用Harzer Roller，我们将插装代码挂钩到函数调用和返回中。挂钩不仅适用于用户应用程序代码，也适用于用于构建固件的SDK。虽然我们保持Harzer Rollergenerally架构的设计独立，但我们提供了基于Xtensa架构的ESP8266 Wi-Fi IoT芯片的实现。我们表明，可以利用Harzer辊跟踪执行流通过库没有可用的源代码，并检测基于堆栈的缓冲区溢出。此外，我们还展示了如何使用溢出检测来转储调试信息以供以后分析。这可以更好地使用各种软件安全测试方法，如无线协议实现的模糊测试或概念验证攻击开发。
2019-12-18 cs.CR
Automated Implementation of Windows-related Security-Configuration Guides
强化是指配置IT系统以确保系统组件及其处理或存储的数据的安全性的过程。然而，当代IT基础设施的复杂性使得手动安全加固和维护成为一项艰巨的任务。在许多组织中，SCAP（安全内容自动化协议）中表达的安全配置指南被用作加强的基础，但这些指南本身并没有提供自动实现所需配置的方法。在本文中，我们提出了一种方法来自动提取相关信息，从公开的安全配置指南Windows操作系统使用自然语言处理。在第二步中，使用存储在Windows管理模板文件中的可用设置的信息来验证提取的信息，其中定义了大多数Windows配置设置。我们表明，我们的实现这种方法可以提取和实现83%的规则，而无需任何手动工作和96%，以最小的手动工作。此外，我们对12个最先进的指南进行了研究，这些指南由2014年的自动检查规则组成，并表明我们的工具至少可以正确实现其中的97%。因此，我们大大减少了基于现有安全配置指南保护系统的工作。
2022-09-19 cs.CR cs.SE
Monografia
制定了综合安全的结构性方案，并制定了创建和开发有效的信息安全系统的原则。
2012-04-15 cs.CR
Embedded Policing and Policy Enforcement based Security in the era of Digital-Physical Convergence for Next-Generation Vehicular Electronics
智能联网车辆的出现，包含复杂的功能，有可能通过提高车辆运输的安全性，保障性和效率，极大地造福社会。这在很大程度上得益于嵌入式系统架构的技术进步，这为汽车制造商提供了实施智能汽车服务并将其整合到少量灵活且可集成的域控制器中的机会。因此，允许越来越集中的操作，包括新的和传统的功能。虽然这个关键和非关键车辆服务的数字-物理融合时代在降低车辆电子设备的成本和电子足迹方面具有优势，但它也带来了重大的安全挑战。解决这一研究问题的一种方法是引入故障转移机制，该机制可以检测由攻击或故障引起的意外或恶意行为，并主动响应控制，最大限度地减少物理损坏或安全隐患。本文提出了一种新的嵌入式警务和策略执行平台架构和伴随的安全建模方法，为下一代车载域控制器。为了证明所提出的方法，连接车辆的案例研究进行。一个现实的攻击场景已被认为是派生的安全策略和建议的安全平台，以提供安全和安全域特定的功能。
2020-04-17 cs.CR eess.SP
Zero Trust Security Model Implementation in Microservices Architectures Using Identity Federation
Unisys Corporation（Unisys公司）；IBM Corporation（IBM公司）；Synechron
本文提出在微服务架构中结合 OIDC、OAuth 2.0 和 SPIFFE/SPIRE 等身份联邦技术实现零信任安全模型，以缩小攻击面、统一策略执行并满足 DevSecOps 要求。
2025-11-07 cs.CR
Cybersecurity through Entropy Injection: A Paradigm Shift from Reactive Defense to Proactive Uncertainty
本文提出熵注入网络安全范式，通过向安全机制注入随机性提升不可预测性，分析其理论基础、实际实现（如ASLR、MTD）及挑战，结果显示能显著降低攻击概率（超90%），实现从被动防御到主动不确定性管理的转变。
2025-04-15 cs.CR
Design Considerations for Building Credible Security Testbeds: A Systematic Study of Industrial Control System Use Cases
本文提出了一个映射框架的设计因素和实施过程，建立可信的工业控制系统（ICS）的安全测试床。在广泛宣传的网络安全事件之后，ICS的弹性已成为运营商和政府的关键问题。无法将传统的信息技术安全做法应用于信息通信系统，进一步加剧了充分保护关键系统的挑战。为了克服这些挑战，并且在不影响现场环境的情况下做到这一点，用于探索、开发和评估安全控制的测试平台被广泛使用。然而，如何设计测试平台及其属性，不仅直接影响其可行性，而且影响其整体可信度。通过结合系统和专题分析和ICS安全测试床设计属性的映射，本文建议，人类实验人员的专业知识，设计目标，实现方法，架构覆盖范围，核心特征和评估方法，是可以帮助建立或增强信心，可信度和接受度的考虑因素，因此，ICS安全测试床的可信度。
2019-11-04 cs.CR
Towards a Context-Aware Security and Privacy as a Service in the Internet of Things
智慧城市是最知名的物联网（IoT）应用之一。智慧城市服务改善了用户的日常生活。然而，安全和隐私问题正在减缓其采用。此外，物联网设备、应用程序和用户的特点使得所考虑的应用程序的安全实现成为一项具有挑战性的任务。为了解决这些问题，我们在本文中提出了一种新的物联网上下文感知安全和隐私架构。由于采用了“即服务”的方法，这种新的架构将以用户为中心。它还将支持已知的上下文感知安全问题：动态性，灵活性。此外，它还将解决移动性，安全和隐私服务的定制，以及对通用物联网应用的支持，特别是对智慧城市的支持。要做到这一点，提出了一个知识平面，允许有效管理的上下文感知。一个安全和隐私平面，允许更好地实现上下文感知的安全和隐私机制也提出了。这将通过基于上下文的微服务的动态组合来实现。还描述了这两个平面的不同组件的作用。
2020-03-04 cs.CR
MPInspector: A Systematic and Automatic Approach for Evaluating the Security of IoT Messaging Protocols
通过消息传递协议（MP）的促进，许多家庭设备连接到互联网，为客户带来便利和可访问性。然而，物联网平台上部署的大多数MP都是分散的，并且没有仔细实施以支持安全通信。据我们所知，目前还没有系统的解决方案来对MP实现执行自动安全检查。为了弥补这一差距，我们提出了MPInspector，这是第一个用于审查MP实现安全性的自动和系统解决方案。MPInspector将模型学习与形式化分析相结合，分为三个阶段：（a）使用参数语义提取和交互逻辑提取来自动推断MP实现的状态机，（b）基于Meta属性和状态机生成安全属性，以及（c）应用基于属性的自动形式化验证来识别属性违规。我们在三个流行的MP上评估了MPInspector，包括MQTT，CoAP和AMQP，这些MP在九个领先的物联网平台上实现。它确定了252个财产违规行为，利用这些违规行为，我们进一步确定了两种现实攻击场景下的11种攻击类型。此外，我们还证明了MPInspector是轻量级的（端到端分析的平均开销约为4.5小时），并且在识别属性违规方面具有100%的精度。
2022-08-18 cs.CR
Verifying Cryptographic Security Implementations in C Using Automated Model Extraction
本文提出了一种自动验证用C语言编写的协议实现的安全属性的方法。我们假设协议的每次成功运行都遵循相同的路径通过C代码，这是由典型的安全协议具有线性结构的事实证明的。然后，我们执行该路径的符号执行，以提取一个类似于CryptoVerif工具所使用的进程演算中表达的模型。符号执行使用一种新的算法，允许符号变量表示潜在未知长度的位串，以模拟传入的协议消息。提取的模型不使用指针寻址内存，但它们可能仍然包含有关消息格式的低级细节。在下一步中，我们用抽象元组和投影运算符替换消息格式化表达式。这些运算符的属性，例如投影运算是元组运算的逆运算，通常只满足正确类型的输入。因此，我们对模型进行类型检查，以确保满足所有类型安全约束。然后，可以使用CryptoVerif来验证所得到的模型，以直接获得计算安全结果，或者使用ProVerif，通过调用计算可靠性定理来获得计算安全结果。我们的方法实现了高度自动化，不需要用户输入超出什么是必要的指定的加密原语的属性和所需的安全目标。我们在几个协议实现上评估了该方法，总共超过3000行代码。最大的案例研究是一个1000行的实现，它是独立编写的，没有考虑验证。我们发现了几个被作者承认并修复的缺陷，并且能够验证修复的代码而无需对其进行任何进一步的修改。
2020-01-03 cs.CR cs.PL
