In recent times, many protocols have been proposed to provide security for various information and communication systems. Such protocols must be tested for their functional correctness before they are used in practice. Application of formal methods for verification of security protocols would enhance their reliability thereby, increasing the usability of systems that employ them. Thus, formal verification of security protocols has become a key issue in computer and communications security. In this paper we present, analyze and compare some prevalent approaches towards verification of secure systems. We follow the notion of - same goal through different approaches - as we formally analyze the Needham Schroeder Public Key protocol for Lowe's attack using each of our presented approaches.
A Logic Programming Approach for Formal Verification of NetBill Security and Transactions Protocol
使用形式化的技术来验证电子商务协议的安全特征将有助于增强此类协议的可靠性，从而提高其可用性。本文提出了应用逻辑编程技术对NetBill协议进行形式化验证的方法。本文采用ALSP（Action Language for Security Protocols）作为有效的形式化规约语言，SMODELS作为模型生成器，对协议进行形式化分析和攻击规划。
We delineate a methodology for the specification and verification of flow security properties expressible in the opacity framework. We propose a logic, OpacTL , for straightforwardly expressing such properties in systems that can be modelled as partially observable labelled transition systems.We develop verification techniques for analysing property opacity with respect to observation notions. Adding a probabilistic operator to the specification language enables quantitative analysis and verification. This analysis is implemented as an extension to the PRISM model checker and illustrated via a…
Accountability is a recent paradigm in security protocol design which aims to eliminate traditional trust assumptions on parties and hold them accountable for their misbehavior. It is meant to establish trust in the first place and to recognize and react if this trust is violated. In this work, we discuss a protocol agnostic definition of accountability: a protocol provides accountability (w.r.t. some security property) if it can identify all misbehaving parties, where misbehavior is defined as a deviation from the protocol that causes a security violation. We provide a mechanized method for t…
In the paper we introduce a process model of security protocols, where processes are graphs with edges labelled by actions, and present a new method of specification and verification of security protocols based on this model.
We present a new and practical framework for security verification of secure architectures. Specifically, we break the verification task into external verification and internal verification. External verification considers the external protocols, i.e. interactions between users, compute servers, network entities, etc. Meanwhile, internal verification considers the interactions between hardware and software components within each server. This verification framework is general-purpose and can be applied to a stand-alone server, or a large-scale distributed system. We evaluate our verification me…
In the world's largest-ever deployment of online voting, the iVote Internet voting system was trusted for the return of 280,000 ballots in the 2015 state election in New South Wales, Australia. During the election, we performed an independent security analysis of parts of the live iVote system and uncovered severe vulnerabilities that could be leveraged to manipulate votes, violate ballot privacy, and subvert the verification mechanism. These vulnerabilities do not seem to have been detected by the election authorities before we disclosed them, despite a pre-election security review and despit…
VANET security introduces significant processing overhead for resource-constrained On-Board Units (OBUs). Here, we propose a novel scheme that allows secure Vehicular Communication (VC) systems to scale well beyond network densities for which existing optimization approaches could be workable, without compromising security (and privacy).
Over the last years, security kernels have played a promising role in reshaping the landscape of platform security on today's ubiquitous embedded devices. Security kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms. They reduce the software portion of the system's trusted computing base to a thin layer, which enforces isolation between low- and high-criticality components. The reduced trusted computing base minimizes the system attack surface and facilitates the use of formal methods to ensure functional correctness and security of the…
Semiconductor design houses are increasingly becoming dependent on third party vendors to procure intellectual property (IP) and meet time-to-market constraints. However, these third party IPs cannot be trusted as hardware Trojans can be maliciously inserted into them by untrusted vendors. While different approaches have been proposed to detect Trojans in third party IPs, their limitations have not been extensively studied. In this paper, we analyze the limitations of the state-of-the-art Trojan detection techniques and demonstrate with experimental results how to defeat these detection mechan…
Even if the verification of authentication protocols can be achieved by means of formal analysis, the modelling of such an activity is an error-prone task due to the lack of automated and integrated processes. This paper proposes a comprehensive approach, based on the Unified Modeling Language (UML) profiling technique and on model-transformation, to enable automatic analysis of authentication protocols starting from high-level models. In particular, a UML-based approach is able to generate an annotated model of communication protocols from which formal notations (e.g., AnBx, Tamarin) can be g…
A large number of crypto accelerators are being deployed with the widespread adoption of IoT. It is vitally important that these accelerators and other security hardware IPs are provably secure. Security is an extra functional requirement and hence many security verification tools are not mature. We propose an approach/flow-PASCAL-that works on RTL designs and discovers potential Timing Side-Channel Attack(SCA) vulnerabilities in them. Based on information flow analysis, this is able to identify Timing Disparate Security Paths that could lead to information leakage. This flow also (automatical…
A Digital Twin (DT) is a digital representation of a physical object used to simulate it before it is built or to predict failures after the object is deployed. In this article, we introduce our approach, which applies the concept of a Cyber Digital Twin (CDT) to automotive software for the purpose of security analysis. In our approach, automotive firmware is transformed into a CDT, which contains automatically extracted, security-relevant information from the firmware. Based on the CDT, we evaluate security requirements through automated analysis and requirements verification using policy enf…
Many widely used Internet messaging and calling apps, such as WhatsApp, Viber, Telegram, and Signal, have deployed an end-to-end encryption functionality. To defeat potential MITM attackers against the key exchange protocol, the approach relies on users to perform a code verification task whereby each user must compare the code (a fingerprint of the cryptographic keys) computed by her app with the one computed by the other user's app and reject the session if the two do not match. In this paper, we study the security and usability of this human-centered code verification task for a setting whe…
Globalization in the semiconductor industry enables fabless design houses to reduce their costs, save time, and make use of newer technologies. However, the offshoring of Integrated Circuit (IC) fabrication has negative sides, including threats such as Hardware Trojans (HTs) - a type of malicious logic that is not trivial to detect. One aspect of IC design that is not affected by globalization is the need for thorough verification. Verification engineers devise complex assets to make sure designs are bug-free, including assertions. This knowledge is typically not reused once verification is ov…
Android is a widely deployed operating system that employs a permission-based access control model. The Android Permissions System (APS) is responsible for mediating resource requests from applications. APS is a critical component of the Android security mechanism. A failure in the design of APS can potentially lead to vulnerabilities that grant unauthorized access to resources by malicious applications. Researchers have employed formal methods for analyzing the security properties of APS. Since Android is constantly evolving, we intend to design and implement a framework for formal specificat…
This paper presents a rewriting logic specification of the Illinois Browser Operating System (IBOS) and defines several security properties, including the same-origin policy (SOP) in reachability logic. It shows how these properties can be deductively verified using our constructor-based reachability logic theorem prover. This paper also highlights the reasoning techniques used in the proof and three modularity principles that have been crucial to scale up and complete the verification effort.
Lack of security expertise among software practitioners is a problem with many implications. First, there is a deficit of security professionals to meet current needs. Additionally, even practitioners who do not plan to work in security may benefit from increased understanding of security. The goal of this paper is to aid software engineering educators in designing a comprehensive software security course by sharing an experience running a software security course for the eleventh time. Through all the eleven years of running the software security course, the course objectives have been compre…
We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and code-level proofs. We automatically translate a Tamarin protocol model into a set of I/O specifications expressed in separation logic. Each such specification describes a protocol role's intended I/O behavior against which the role's implementation is then verified. Our soundness result guarantees that the verified implementation inherits all security (trace) properties proved for the Tamarin model. Our framework th…
ZKP Security Tools and Verification: Coverage, Effectiveness, Adoption, and Challenges
Max Planck Institute for Security and Privacy (MPI-SP)（马克斯·普朗克安全与隐私研究所）；KTH Royal Institute of Technology（皇家理工学院）；Ethereum Foundation（以太坊基金会）；University of Athens & zkSecurity（雅典大学与zkSecurity）
The Internet of Vehicles (IoV) equips vehicles with connectivity to the Internet and the Internet of Things (IoT) to support modern applications such as autonomous driving. However, the consolidation of complex computing domains of vehicles, the Internet, and the IoT limits the applicability of tailored security solutions. In this paper, we propose a new methodology to quantitatively verify the security of single or system-level assets of the IoV infrastructure. In detail, our methodology decomposes assets of the IoV infrastructure with the help of reference sub-architectures and the 4+1 view …
As software becomes more complex and assumes an even greater role in our lives, formal verification is set to become the gold standard in securing software systems into the future, since it can guarantee the absence of errors and entire classes of attack. Recent advances in formal verification are being used to secure everything from unmanned drones to the internet. At the same time, the usable security research community has made huge progress in improving the usability of security products and end-users comprehension of security issues. However, there have been no human-centered studies focu…
Programmable Logic Controllers (PLCs) play a critical role in the industrial control systems. Vulnerabilities in PLC programs might lead to attacks causing devastating consequences to the critical infrastructure, as shown in Stuxnet and similar attacks. In recent years, we have seen an exponential increase in vulnerabilities reported for PLC control logic. Looking back on past research, we found extensive studies explored control logic modification attacks, as well as formal verification-based security solutions. We performed systematization on these studies, and found attacks that can comprom…
Software defined networking (SDN) has been adopted to enforce the security of large-scale and complex networks because of its programmable, abstract, centralized intelligent control and global and real-time traffic view. However, the current SDN-based security enforcement mechanisms require network managers to fully understand the underlying configurations of network. Facing the increasingly complex and huge SDN networks, we urgently need a novel security policy management mechanism which can be completely transparent to any underlying information. That is it can permit network managers to def…
This work presents the first full implementation of Wave, a postquantum code-based signature scheme. We define Wavelet, a concrete Wave scheme at the 128-bit classical security level (or NIST postquantum security Level 1) equipped with a fast verification algorithm targeting embedded devices. Wavelet offers 930-byte signatures, with a public key of 3161 kB. We include implementation details using AVX instructions, and on ARM Cortex-M4, including a solution to deal with Wavelet's large public keys, which do not fit in the SRAM of a typical embedded device. Our verification algorithm is $\approx…
Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges that we address in this paper. We model the semantics of trusted computing platforms (including CPU, TPM, OS, and other essential components) and of associated protocols in a classical process calculus accepted by ProVerif. As part of the formalization effort, we introduce new equational theories for representing TPM specific platform states and dynamically loaded programs. Formal models for such an extensive set of features cannot be rea…
The proliferation of Unmanned Aerial Vehicles (UAVs) embedded with vulnerable monolithic software has recently raised serious concerns about their security due to concurrency aspects and fragile communication links. However, verifying security in UAV software based on traditional testing remains an open challenge mainly due to scalability and deployment issues. Here we investigate software verification techniques to detect security vulnerabilities in typical UAVs. In particular, we investigate existing software analyzers and verifiers, which implement fuzzing and bounded model checking (BMC) t…
EarthOL: A Proof-of-Human-Contribution Consensus Protocol -- Addressing Fundamental Challenges in Decentralized Value Assessment with Enhanced Verification and Security Mechanisms
