Visible to the public Biblio

Filters: Keyword is formal verification  [Clear All Filters]
Kulik, T., Tran-Jørgensen, P. W. V., Boudjadar, J., Schultz, C..  2018.  A Framework for Threat-Driven Cyber Security Verification of IoT Systems. 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). :89-97.

Industrial control systems are changing from monolithic to distributed and interconnected architectures, entering the era of industrial IoT. One fundamental issue is that security properties of such distributed control systems are typically only verified empirically, during development and after system deployment. We propose a novel modelling framework for the security verification of distributed industrial control systems, with the goal of moving towards early design stage formal verification. In our framework we model industrial IoT infrastructures, attack patterns, and mitigation strategies for countering attacks. We conduct model checking-based formal analysis of system security through scenario execution, where the analysed system is exposed to attacks and implement mitigation strategies. We study the applicability of our framework for large systems using a scalability analysis.

Plasencia-Balabarca, F., Mitacc-Meza, E., Raffo-Jara, M., Silva-Cárdenas, C..  2018.  Robust Functional Verification Framework Based in UVM Applied to an AES Encryption Module. 2018 New Generation of CAS (NGCAS). :194-197.

This Since the past century, the digital design industry has performed an outstanding role in the development of electronics. Hence, a great variety of designs are developed daily, these designs must be submitted to high standards of verification in order to ensure the 100% of reliability and the achievement of all design requirements. The Universal Verification Methodology (UVM) is the current standard at the industry for the verification process due to its reusability, scalability, time-efficiency and feasibility of handling high-level designs. This research proposes a functional verification framework using UVM for an AES encryption module based on a very detailed and robust verification plan. This document describes the complete verification process as done in the industry for a popular module used in information-security applications in the field of cryptography, defining the basis for future projects. The overall results show the achievement of the high verification standards required in industry applications and highlight the advantages of UVM against System Verilog-based functional verification and direct verification methodologies previously developed for the AES module.

Park, Daejun, Zhang, Yi, Saxena, Manasvi, Daian, Philip, Ro\c su, Grigore.  2018.  A Formal Verification Tool for Ethereum VM Bytecode. Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. :912-915.

In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.

Hu, W., Ardeshiricham, A., Gobulukoglu, M. S., Wang, X., Kastner, R..  2018.  Property Specific Information Flow Analysis for Hardware Security Verification. 2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). :1-8.

Hardware information flow analysis detects security vulnerabilities resulting from unintended design flaws, timing channels, and hardware Trojans. These information flow models are typically generated in a general way, which includes a significant amount of redundancy that is irrelevant to the specified security properties. In this work, we propose a property specific approach for information flow security. We create information flow models tailored to the properties to be verified by performing a property specific search to identify security critical paths. This helps find suspicious signals that require closer inspection and quickly eliminates portions of the design that are free of security violations. Our property specific trimming technique reduces the complexity of the security model; this accelerates security verification and restricts potential security violations to a smaller region which helps quickly pinpoint hardware security vulnerabilities.

Neal, T., Sundararajan, K., Woodard, D..  2018.  Exploiting Linguistic Style as a Cognitive Biometric for Continuous Verification. 2018 International Conference on Biometrics (ICB). :270-276.
This paper presents an assessment of continuous verification using linguistic style as a cognitive biometric. In stylometry, it is widely known that linguistic style is highly characteristic of authorship using representations that capture authorial style at character, lexical, syntactic, and semantic levels. In this work, we provide a contrast to previous efforts by implementing a one-class classification problem using Isolation Forests. Our approach demonstrates the usefulness of this classifier for accurately verifying the genuine user, and yields recognition accuracy exceeding 98% using very small training samples of 50 and 100-character blocks.
Nichols, W., Hawrylak, P. J., Hale, J., Papa, M..  2018.  Methodology to Estimate Attack Graph System State from a Simulation of a Nuclear Research Reactor. 2018 Resilience Week (RWS). :84-87.
Hybrid attack graphs are a powerful tool when analyzing the cybersecurity of a cyber-physical system. However, it is important to ensure that this tool correctly models reality, particularly when modelling safety-critical applications, such as a nuclear reactor. By automatically verifying that a simulation reaches the state predicted by an attack graph by analyzing the final state of the simulation, this verification procedure can be accomplished. As such, a mechanism to estimate if a simulation reaches the expected state in a hybrid attack graph is proposed here for the nuclear reactor domain.
Ye, Katherine Q., Green, Matthew, Sanguansin, Naphat, Beringer, Lennart, Petcher, Adam, Appel, Andrew W..  2017.  Verified Correctness and Security of mbedTLS HMAC-DRBG. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. :2007–2020.
We have formalized the functional specification of HMAC-DRBG (NIST 800-90A), and we have proved its cryptographic security-that its output is pseudorandom–using a hybrid game-based proof. We have also proved that the mbedTLS implementation (C program) correctly implements this functional specification. That proof composes with an existing C compiler correctness proof to guarantee, end-to-end, that the machine language program gives strong pseudorandomness. All proofs (hybrid games, C program verification, compiler, and their composition) are machine-checked in the Coq proof assistant. Our proofs are modular: the hybrid game proof holds on any implementation of HMAC-DRBG that satisfies our functional specification. Therefore, our functional specification can serve as a high-assurance reference.
Matsuo, S..  2017.  How formal analysis and verification add security to blockchain-based systems. 2017 Formal Methods in Computer Aided Design (FMCAD). :1–4.

Blockchain is an integrated technology to ensure keeping record and process transactions with decentralized manner. It is thought as the foundation of future decentralized ecosystem, and collects much attention. However, the maturity of this technology including security of the fundamental protocol and its applications is not enough, thus we need more research on the security evaluation and verification of Blockchain technology This tutorial explains the current status of the security of this technology, its security layers and possibility of application of formal analysis and verification.

Guo, X., Dutta, R. G., He, J., Jin, Y..  2017.  PCH framework for IP runtime security verification. 2017 Asian Hardware Oriented Security and Trust Symposium (AsianHOST). :79–84.

Untrusted third-party vendors and manufacturers have raised security concerns in hardware supply chain. Among all existing solutions, formal verification methods provide powerful solutions in detection malicious behaviors at the pre-silicon stage. However, little work have been done towards built-in hardware runtime verification at the post-silicon stage. In this paper, a runtime formal verification framework is proposed to evaluate the trust of hardware during its execution. This framework combines the symbolic execution and SAT solving methods to validate the user defined properties. The proposed framework has been demonstrated on an FPGA platform using an SoC design with untrusted IPs. The experimentation results show that the proposed approach can provide high-level security assurance for hardware at runtime.

Antignac, Thibaud, Mukelabai, Mukelabai, Schneider, Gerardo.  2017.  Specification, Design, and Verification of an Accountability-aware Surveillance Protocol. Proceedings of the Symposium on Applied Computing. :1372–1378.

Though controversial, surveillance activities are more and more performed for security reasons. However, such activities are extremely privacy-intrusive. This is seen as a necessary side-effect to ensure the success of such operations. In this paper, we propose an accountability-aware protocol designed for surveillance purposes. It relies on a strong incentive for a surveillance organisation to register its activity to a data protection authority. We first elicit a list of account-ability requirements, we provide an architecture showing the interaction of the different involved parties, and we propose an accountability-aware protocol which is formally specified in the applied pi calculus. We use the ProVerif tool to automatically verify that the protocol respects confidentiality, integrity and authentication properties.

Kang, E. Y., Mu, D., Huang, L., Lan, Q..  2017.  Verification and Validation of a Cyber-Physical System in the Automotive Domain. 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :326–333.
Software development for Cyber-Physical Systems (CPS), e.g., autonomous vehicles, requires both functional and non-functional quality assurance to guarantee that the CPS operates safely and effectively. EAST-ADL is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time (ERT) behaviors modeled in EAST-ADL/Stateflow into UPPAAL models amenable to formal verification. Previous work is extended in this paper by including support for Simulink and an integration of Simulink/Stateflow (S/S) within the same too lchain. S/S models are transformed, based on the extended ERT constraints with probability parameters, into verifiable UPPAAL-SMC models and integrate the translation with formal statistical analysis techniques: Probabilistic extension of EAST-ADL constraints is defined as a semantics denotation. A set of mapping rules is proposed to facilitate the guarantee of translation. Formal analysis on both functional- and non-functional properties is performed using Simulink Design Verifier and UPPAAL-SMC. Our approach is demonstrated on the autonomous traffic sign recognition vehicle case study.
Joshaghani, R., Mehrpouyan, H..  2017.  A Model-Checking Approach for Enforcing Purpose-Based Privacy Policies. 2017 IEEE Symposium on Privacy-Aware Computing (PAC). :178–179.

With the growth of Internet in many different aspects of life, users are required to share private information more than ever. Hence, users need a privacy management tool that can enforce complex and customized privacy policies. In this paper, we propose a privacy management system that not only allows users to define complex privacy policies for data sharing actions, but also monitors users' behavior and relationships to generate realistic policies. In addition, the proposed system utilizes formal modeling and model-checking approach to prove that information disclosures are valid and privacy policies are consistent with one another.

Kobeissi, N., Bhargavan, K., Blanchet, B..  2017.  Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. 2017 IEEE European Symposium on Security and Privacy (EuroS P). :435–450.

Many popular web applications incorporate end-toend secure messaging protocols, which seek to ensure that messages sent between users are kept confidential and authenticated, even if the web application's servers are broken into or otherwise compelled into releasing all their data. Protocols that promise such strong security guarantees should be held up to rigorous analysis, since protocol flaws and implementations bugs can easily lead to real-world attacks. We propose a novel methodology that allows protocol designers, implementers, and security analysts to collaboratively verify a protocol using automated tools. The protocol is implemented in ProScript, a new domain-specific language that is designed for writing cryptographic protocol code that can both be executed within JavaScript programs and automatically translated to a readable model in the applied pi calculus. This model can then be analyzed symbolically using ProVerif to find attacks in a variety of threat models. The model can also be used as the basis of a computational proof using CryptoVerif, which reduces the security of the protocol to standard cryptographic assumptions. If ProVerif finds an attack, or if the CryptoVerif proof reveals a weakness, the protocol designer modifies the ProScript protocol code and regenerates the model to enable a new analysis. We demonstrate our methodology by implementing and analyzing a variant of the popular Signal Protocol with only minor differences. We use ProVerif and CryptoVerif to find new and previously-known weaknesses in the protocol and suggest practical countermeasures. Our ProScript protocol code is incorporated within the current release of Cryptocat, a desktop secure messenger application written in JavaScript. Our results indicate that, with disciplined programming and some verification expertise, the systematic analysis of complex cryptographic web applications is now becoming practical.

Genge, B., Duka, A. V., Haller, P., Crainicu, B., Sándor, H., Graur, F..  2017.  Design, Verification and Implementation of a Lightweight Remote Attestation Protocol for Process Control Systems. 2017 IEEE 15th International Conference on Industrial Informatics (INDIN). :75–82.

Until recently, IT security received limited attention within the scope of Process Control Systems (PCS). In the past, PCS consisted of isolated, specialized components running closed process control applications, where hardware was placed in physically secured locations and connections to remote network infrastructures were forbidden. Nowadays, industrial communications are fully exploiting the plethora of features and novel capabilities deriving from the adoption of commodity off the shelf (COTS) hardware and software. Nonetheless, the reliance on COTS for remote monitoring, configuration and maintenance also exposed PCS to significant cyber threats. In light of these issues, this paper presents the steps for the design, verification and implementation of a lightweight remote attestation protocol. The protocol is aimed at providing a secure software integrity verification scheme that can be readily integrated into existing industrial applications. The main novelty of the designed protocol is that it encapsulates key elements for the protection of both participating parties (i.e., verifier and prover) against cyber attacks. The protocol is formally verified for correctness with the help of the Scyther model checking tool. The protocol implementation and experimental results are provided for a Phoenix-Contact industrial controller, which is widely used in the automation of gas transportation networks in Romania.

Hamouda, R. Ben, Hafaiedh, I. Ben.  2017.  Formal Modeling and Verification of a Wireless Body Area Network (WBAN) Protocol: S-TDMA Protocol. 2017 International Conference on Internet of Things, Embedded Systems and Communications (IINTEC). :72–77.

WBANs integrate wearable and implanted devices with wireless communication and information processing systems to monitor the well-being of an individual. Various MAC (Medium Access Control) protocols with different objectives have been proposed for WBANs. The fact that any flaw in these critical systems may lead to the loss of one's life implies that testing and verifying MAC's protocols for such systems are on the higher level of importance. In this paper, we firstly propose a high-level formal and scalable model with timing aspects for a MAC protocol particularly designed for WBANs, named S-TDMA (Statistical frame based TDMA protocol). The protocol uses TDMA (Time Division Multiple Access) bus arbitration, which requires temporal aspect modeling. Secondly, we propose a formal validation of several relevant properties such as deadlock freedom, fairness and mutual exclusion of this protocol at a high level of abstraction. The protocol was modeled using a composition of timed automata components, and verification was performed using a real-time model checker.

Tripathy, B. K., Sudhir, A., Bera, P., Rahman, M. A..  2017.  Formal Modelling and Verification of Requirements of Adaptive Routing Protocol for Mobile Ad-Hoc Network. 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC). 1:548–556.

A group of mobile nodes with limited capabilities sparsed in different clusters forms the backbone of Mobile Ad-Hoc Networks (MANET). In such situations, the requirements (mobility, performance, security, trust and timing constraints) vary with change in context, time, and geographic location of deployment. This leads to various performance and security challenges which necessitates a trade-off between them on the application of routing protocols in a specific context. The focus of our research is towards developing an adaptive and secure routing protocol for Mobile Ad-Hoc Networks, which dynamically configures the routing functions using varying contextual features with secure and real-time processing of traffic. In this paper, we propose a formal framework for modelling and verification of requirement constraints to be used in designing adaptive routing protocols for MANET. We formally represent the network topology, behaviour, and functionalities of the network in SMT-LIB language. In addition, our framework verifies various functional, security, and Quality-of-Service (QoS) constraints. The verification engine is built using the Yices SMT Solver. The efficacy of the proposed requirement models is demonstrated with experimental results.

Schnepf, N., Badonnel, R., Lahmadi, A., Merz, S..  2017.  Automated Verification of Security Chains in Software-Defined Networks with Synaptic. 2017 IEEE Conference on Network Softwarization (NetSoft). :1–9.

Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.

Schnepf, N., Badonnel, R., Lahmadi, A., Merz, S..  2017.  Automated Verification of Security Chains in Software-Defined Networks with Synaptic. 2017 IEEE Conference on Network Softwarization (NetSoft). :1–9.
Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers.
Sugumar, G., Mathur, A..  2017.  Testing the Effectiveness of Attack Detection Mechanisms in Industrial Control Systems. 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :138–145.

Industrial Control Systems (ICS) are found in critical infrastructure such as for power generation and water treatment. When security requirements are incorporated into an ICS, one needs to test the additional code and devices added do improve the prevention and detection of cyber attacks. Conducting such tests in legacy systems is a challenge due to the high availability requirement. An approach using Timed Automata (TA) is proposed to overcome this challenge. This approach enables assessment of the effectiveness of an attack detection method based on process invariants. The approach has been demonstrated in a case study on one stage of a 6- stage operational water treatment plant. The model constructed captured the interactions among components in the selected stage. In addition, a set of attacks, attack detection mechanisms, and security specifications were also modeled using TA. These TA models were conjoined into a network and implemented in UPPAAL. The models so implemented were found effective in detecting the attacks considered. The study suggests the use of TA as an effective tool to model an ICS and study its attack detection mechanisms as a complement to doing so in a real plant-operational or under design.

Baldi, M., Chiaraluce, F., Senigagliesi, L., Spalazzi, L., Spegni, F..  2017.  Security in Heterogeneous Distributed Storage Systems: A Practically Achievable Information-Theoretic Approach. 2017 IEEE Symposium on Computers and Communications (ISCC). :1021–1028.

Distributed storage systems and caching systems are becoming widespread, and this motivates the increasing interest on assessing their achievable performance in terms of reliability for legitimate users and security against malicious users. While the assessment of reliability takes benefit of the availability of well established metrics and tools, assessing security is more challenging. The classical cryptographic approach aims at estimating the computational effort for an attacker to break the system, and ensuring that it is far above any feasible amount. This has the limitation of depending on attack algorithms and advances in computing power. The information-theoretic approach instead exploits capacity measures to achieve unconditional security against attackers, but often does not provide practical recipes to reach such a condition. We propose a mixed cryptographic/information-theoretic approach with a twofold goal: estimating the levels of information-theoretic security and defining a practical scheme able to achieve them. In order to find optimal choices of the parameters of the proposed scheme, we exploit an effective probabilistic model checker, which allows us to overcome several limitations of more conventional methods.

Hess, A. V., Mödersheim, S..  2017.  Formalizing and Proving a Typing Result for Security Protocols in Isabelle/HOL. 2017 IEEE 30th Computer Security Foundations Symposium (CSF). :451–463.

There are several works on the formalization of security protocols and proofs of their security in Isabelle/HOL; there have also been tools for automatically generating such proofs. This is attractive since a proof in Isabelle gives a higher assurance of the correctness than a pen-and-paper proof or the positive output of a verification tool. However several of these works have used a typed model, where the intruder is restricted to "well-typed" attacks. There also have been several works that show that this is actually not a restriction for a large class of protocols, but all these results so far are again pen-and-paper proofs. In this work we present a formalization of such a typing result in Isabelle/HOL. We formalize a constraint-based approach that is used in the proof argument of such typing results, and prove its soundness, completeness and termination. We then formalize and prove the typing result itself in Isabelle. Finally, to illustrate the real-world feasibility, we prove that the standard Transport Layer Security (TLS) handshake satisfies the main condition of the typing result.

Ramadan, Q., Salnitriy, M., Strüber, D., Jürjens, J., Giorgini, P..  2017.  From Secure Business Process Modeling to Design-Level Security Verification. 2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS). :123–133.

Tracing and integrating security requirements throughout the development process is a key challenge in security engineering. In socio-technical systems, security requirements for the organizational and technical aspects of a system are currently dealt with separately, giving rise to substantial misconceptions and errors. In this paper, we present a model-based security engineering framework for supporting the system design on the organizational and technical level. The key idea is to allow the involved experts to specify security requirements in the languages they are familiar with: business analysts use BPMN for procedural system descriptions; system developers use UML to design and implement the system architecture. Security requirements are captured via the language extensions SecBPMN2 and UMLsec. We provide a model transformation to bridge the conceptual gap between SecBPMN2 and UMLsec. Using UMLsec policies, various security properties of the resulting architecture can be verified. In a case study featuring an air traffic management system, we show how our framework can be practically applied.

Madhusudhanan, S., Mallissery, S..  2017.  Provable security analysis of complex or smart computer systems in the smart grid. 2017 IEEE International Conference on Smart Grid and Smart Cities (ICSGSC). :210–214.

Security is an important requirement of every reactive system of the smart gird. The devices connected to the smart system in smart grid are exhaustively used to provide digital information to outside world. The security of such a system is an essential requirement. The most important component of such smart systems is Operating System (OS). This paper mainly focuses on the security of OS by incorporating Access Control Mechanism (ACM) which will improve the efficiency of the smart system. The formal methods use applied mathematics for modelling and analysing of smart systems. In the proposed work Formal Security Analysis (FSA) is used with model checking and hence it helped to prove the security of smart systems. When an Operating System (OS) takes into consideration, it never comes to a halt state. In the proposed work a Transition System (TS) is designed and the desired rules of security are provided by using Linear Temporal Logics (LTL). Unlike other propositional and predicate logic, LTL can model reactive systems with a prediction for the future state of the systems. In the proposed work, Simple Promela Interpreter (SPIN) is used as a model checker that takes LTL and TS of the system as input. Hence it is possible to derive the Büchi automaton from LTL logics and that provides traces of both successful and erroneous computations. Comparison of Büchi automaton with the transition behaviour of the OS will provide the details of security violation in the system. Validation of automaton operations on infinite computational sequences verify that whether systems are provably secure or not. Hence the proposed formal security analysis will provably ensures the security of smart systems in the area of smart grid applications.

Subramanyan, Pramod, Sinha, Rohit, Lebedev, Ilia, Devadas, Srinivas, Seshia, Sanjit A..  2017.  A Formal Foundation for Secure Remote Execution of Enclaves. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. :2435–2450.

Recent proposals for trusted hardware platforms, such as Intel SGX and the MIT Sanctum processor, offer compelling security features but lack formal guarantees. We introduce a verification methodology based on a trusted abstract platform (TAP), a formalization of idealized enclave platforms along with a parameterized adversary. We also formalize the notion of secure remote execution and present machine-checked proofs showing that the TAP satisfies the three key security properties that entail secure remote execution: integrity, confidentiality and secure measurement. We then present machine-checked proofs showing that SGX and Sanctum are refinements of the TAP under certain parameterizations of the adversary, demonstrating that these systems implement secure enclaves for the stated adversary models.

Delaune, S., Kremer, S., Robin, L..  2017.  Formal Verification of Protocols Based on Short Authenticated Strings. 2017 IEEE 30th Computer Security Foundations Symposium (CSF). :130–143.
Modern security protocols may involve humans in order to compare or copy short strings between different devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-secure are typical examples of such protocols. However, such short strings may be subject to brute force attacks. In this paper we propose a symbolic model which includes attacker capabilities for both guessing short strings, and producing collisions when short strings result from an application of weak hash functions. We propose a new decision procedure for analysing (a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in the AKISS tool and tested on protocols from the ISO/IEC 9798-6:2010 standard.