Visible to the public Biblio

Found 102 results

Filters: Keyword is formal verification  [Clear All Filters]
Journal Article
Qadir, J., Hasan, O..  2015.  Applying Formal Methods to Networking: Theory, Techniques, and Applications. Communications Surveys Tutorials, IEEE. 17:256-291.

Despite its great importance, modern network infrastructure is remarkable for the lack of rigor in its engineering. The Internet, which began as a research experiment, was never designed to handle the users and applications it hosts today. The lack of formalization of the Internet architecture meant limited abstractions and modularity, particularly for the control and management planes, thus requiring for every new need a new protocol built from scratch. This led to an unwieldy ossified Internet architecture resistant to any attempts at formal verification and to an Internet culture where expediency and pragmatism are favored over formal correctness. Fortunately, recent work in the space of clean slate Internet design-in particular, the software defined networking (SDN) paradigm-offers the Internet community another chance to develop the right kind of architecture and abstractions. This has also led to a great resurgence in interest of applying formal methods to specification, verification, and synthesis of networking protocols and applications. In this paper, we present a self-contained tutorial of the formidable amount of work that has been done in formal methods and present a survey of its applications to networking.
 

J. Qadir, O. Hasan.  2015.  "Applying Formal Methods to Networking: Theory, Techniques, and Applications". IEEE Communications Surveys Tutorials. 17:256-291.

Despite its great importance, modern network infrastructure is remarkable for the lack of rigor in its engineering. The Internet, which began as a research experiment, was never designed to handle the users and applications it hosts today. The lack of formalization of the Internet architecture meant limited abstractions and modularity, particularly for the control and management planes, thus requiring for every new need a new protocol built from scratch. This led to an unwieldy ossified Internet architecture resistant to any attempts at formal verification and to an Internet culture where expediency and pragmatism are favored over formal correctness. Fortunately, recent work in the space of clean slate Internet design-in particular, the software defined networking (SDN) paradigm-offers the Internet community another chance to develop the right kind of architecture and abstractions. This has also led to a great resurgence in interest of applying formal methods to specification, verification, and synthesis of networking protocols and applications. In this paper, we present a self-contained tutorial of the formidable amount of work that has been done in formal methods and present a survey of its applications to networking.

Huaqun Wang.  2015.  Identity-Based Distributed Provable Data Possession in Multicloud Storage. Services Computing, IEEE Transactions on. 8:328-340.

Remote data integrity checking is of crucial importance in cloud storage. It can make the clients verify whether their outsourced data is kept intact without downloading the whole data. In some application scenarios, the clients have to store their data on multicloud servers. At the same time, the integrity checking protocol must be efficient in order to save the verifier's cost. From the two points, we propose a novel remote data integrity checking model: ID-DPDP (identity-based distributed provable data possession) in multicloud storage. The formal system model and security model are given. Based on the bilinear pairings, a concrete ID-DPDP protocol is designed. The proposed ID-DPDP protocol is provably secure under the hardness assumption of the standard CDH (computational Diffie-Hellman) problem. In addition to the structural advantage of elimination of certificate management, our ID-DPDP protocol is also efficient and flexible. Based on the client's authorization, the proposed ID-DPDP protocol can realize private verification, delegated verification, and public verification.
 

Subramanyan, P., Tsiskaridze, N., Wenchao Li, Gascon, A., Wei Yang Tan, Tiwari, A., Shankar, N., Seshia, S.A., Malik, S..  2014.  Reverse Engineering Digital Circuits Using Structural and Functional Analyses. Emerging Topics in Computing, IEEE Transactions on. 2:63-80.

Integrated circuits (ICs) are now designed and fabricated in a globalized multivendor environment making them vulnerable to malicious design changes, the insertion of hardware Trojans/malware, and intellectual property (IP) theft. Algorithmic reverse engineering of digital circuits can mitigate these concerns by enabling analysts to detect malicious hardware, verify the integrity of ICs, and detect IP violations. In this paper, we present a set of algorithms for the reverse engineering of digital circuits starting from an unstructured netlist and resulting in a high-level netlist with components such as register files, counters, adders, and subtractors. Our techniques require no manual intervention and experiments show that they determine the functionality of >45% and up to 93% of the gates in each of the test circuits that we examine. We also demonstrate that our algorithms are scalable to real designs by experimenting with a very large, highly-optimized system-on-chip (SOC) design with over 375000 combinational elements. Our inference algorithms cover 68% of the gates in this SOC. We also demonstrate that our algorithms are effective in aiding a human analyst to detect hardware Trojans in an unstructured netlist.
 

Conference Paper
Laranjeiro, Nuno, Gomez, Camilo, Schiavone, Enrico, Montecchi, Leonardo, Carvalho, Manoel J. M., Lollini, Paolo, Micskei, Zoltán.  2019.  Addressing Verification and Validation Challenges in Future Cyber-Physical Systems. 2019 9th Latin-American Symposium on Dependable Computing (LADC). :1–2.
Cyber-physical systems are characterized by strong interactions between their physical and computation parts. The increasing complexity of such systems, now used in numerous application domains (e.g., aeronautics, healthcare), in conjunction with hard to predict surrounding environments or the use of non-traditional middleware and with the presence of non-deterministic or non-explainable software outputs, tend to make traditional Verification and Validation (V&V) techniques ineffective. This paper presents the H2020 ADVANCE project, which aims precisely at addressing the Verification and Validation challenges that the next-generation of cyber-physical systems bring, by exploring techniques, methods and tools for achieving the technical objective of improving the overall efficiency and effectiveness of the V&V process. From a strategic perspective, the goal of the project is to create an international network of expertise on the topic of V&V of cyber-physical systems.
Kwiatkowska, M..  2016.  Advances and challenges of quantitative verification and synthesis for cyber-physical systems. 2016 Science of Security for Cyber-Physical Systems Workshop (SOSCYPS). :1–5.

We are witnessing a huge growth of cyber-physical systems, which are autonomous, mobile, endowed with sensing, controlled by software, and often wirelessly connected and Internet-enabled. They include factory automation systems, robotic assistants, self-driving cars, and wearable and implantable devices. Since they are increasingly often used in safety- or business-critical contexts, to mention invasive treatment or biometric authentication, there is an urgent need for modelling and verification technologies to support the design process, and hence improve the reliability and reduce production costs. This paper gives an overview of quantitative verification and synthesis techniques developed for cyber-physical systems, summarising recent achievements and future challenges in this important field.

Zhang, Yong, Liu, Yingjie.  2019.  Application of STPA in Temporary Speed Restriction Sending Scenario of Train Control System Based on Vehicle-Vehicle Communication. 2019 5th International Conference on Control Science and Systems Engineering (ICCSSE). :99—103.
In this paper, System Theoretic Process Analysis (STPA) method was used to analyze the security of Temporary Speed Restriction (TSR) sending scenario in train control system based on vehicle-vehicle communication. The security of this scenario was analyzed according to the analysis process of STPA method. Firstly, Unsafe Control Actions (UCAs) in this scenario were identified and Control Defects (CDs) were analyzed. After that, the corresponding Security Design Requirements (SDRs) were formulated according to the obtained control defects. Finally, the time automata network model of TSR sending scenario was established to verify SDRs. The result shows that: STPA method is suitable to discover the unsafe factors and safety hazards of train control system and take corresponding safety measures to prevent the occurrence of accidents.
Rathmair, M., Schupfer, F., Krieg, C..  2014.  Applied formal methods for hardware Trojan detection. Circuits and Systems (ISCAS), 2014 IEEE International Symposium on. :169-172.

This paper addresses the potential danger using integrated circuits which contain malicious hardware modifications hidden in the silicon structure. A so called hardware Trojan may be added at several stages of the chip development process. This work concentrates on formal hardware Trojan detection during the design phase and highlights applied verification techniques. Selected methods are discussed and their combination used to increase an introduced “Trojan Assurance Level”.
 

Mahale, Anusha, B.S., Kariyappa.  2019.  Architecture Analysis and Verification of I3C Protocol. 2019 3rd International Conference on Electronics, Communication and Aerospace Technology (ICECA). :930-935.

In VLSI industry the design cycle is categorized into Front End Design and Back End Design. Front End Design flow is from Specifications to functional verification of RTL design. Back End Design is from logic synthesis to fabrication of chip. Handheld devices like Mobile SOC's is an amalgamation of many components like GPU, camera, sensor, display etc. on one single chip. In order to integrate these components protocols are needed. One such protocol in the emerging trend is I3C protocol. I3C is abbreviated as Improved Inter Integrated Circuit developed by Mobile Industry Processor Interface (MIPI) alliance. Most probably used for the interconnection of sensors in Mobile SOC's. The main motivation of adapting the standard is for the increase speed and low pin count in most of the hardware chips. The bus protocol is backward compatible with I2C devices. The paper includes detailed study I3C bus protocol and developing verification environment for the protocol. The test bench environment is written and verified using system Verilog and UVM. The Universal Verification Methodology (UVM) is base class library built using System Verilog which provides the fundamental blocks needed to quickly develop reusable and well-constructed verification components and test environments. The Functional Coverage of around 93.55 % and Code Coverage of around 98.89 % is achieved by verification closure.

Deb Nath, Atul Prasad, Bhunia, Swarup, Ray, Sandip.  2018.  ArtiFact: Architecture and CAD Flow for Efficient Formal Verification of SoC Security Policies. 2018 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). :411–416.
Verification of security policies represents one of the most critical, complex, and expensive steps of modern SoC design validation. SoC security policies are typically implemented as part of functional design flow, with a diverse set of protection mechanisms sprinkled across various IP blocks. An obvious upshot is that their verification requires comprehension and analysis of the entire system, representing a scalability bottleneck for verification tools. The scale and complexity of industrial SoC is far beyond the analysis capacity of state-of-the-art formal tools; even simulation-based security verification is severely limited in effectiveness because of the need to exercise subtle corner-cases across the entire system. We address this challenge by developing a novel security architecture that accounts for verification needs from the ground up. Our framework, ArtiFact, provides an alternative architecture for security policy implementation that exploits a flexible, centralized, infrastructure IP and enables scalable, streamlined verification of these policies. With our architecture, verification of system-level security policies reduces to analysis of this single IP and its interfaces, enabling off-the-shelf formal tools to successfully verify these policies. We introduce a CAD flow that supports both formal and dynamic (simulation-based) verification, and is built on top of such off-the-shelf tools. Our approach reduces verification time by over 62X and bug detection time by 34X for illustrative policies.
Emeka, Busalire Onesmus, Liu, Shaoying.  2018.  Assessing and extracting software security vulnerabilities in SOFL formal specifications. 2018 International Conference on Electronics, Information, and Communication (ICEIC). :1—4.

The growth of the internet has brought along positive gains such as the emergence of a highly interconnected world. However, on the flip side, there has been a growing concern on how secure distributed systems can be built effectively and tested for security vulnerabilities prior to deployment. Developing a secure software product calls for a deep technical understanding of some complex issues with regards to the software and its operating environment, as well as embracing a systematic approach of analyzing the software. This paper proposes a method for identifying software security vulnerabilities from software requirement specifications written in Structured Object-oriented Formal Language (SOFL). Our proposed methodology leverages on the concept of providing an early focus on security by identifying potential security vulnerabilities at the requirement analysis and verification phase of the software development life cycle.

Madi, Taous, Majumdar, Suryadipta, Wang, Yushun, Jarraya, Yosr, Pourzandi, Makan, Wang, Lingyu.  2016.  Auditing Security Compliance of the Virtualized Infrastructure in the Cloud: Application to OpenStack. Proceedings of the Sixth ACM Conference on Data and Application Security and Privacy. :195–206.

Cloud service providers typically adopt the multi-tenancy model to optimize resources usage and achieve the promised cost-effectiveness. Sharing resources between different tenants and the underlying complex technology increase the necessity of transparency and accountability. In this regard, auditing security compliance of the provider's infrastructure against standards, regulations and customers' policies takes on an increasing importance in the cloud to boost the trust between the stakeholders. However, virtualization and scalability make compliance verification challenging. In this work, we propose an automated framework that allows auditing the cloud infrastructure from the structural point of view while focusing on virtualization-related security properties and consistency between multiple control layers. Furthermore, to show the feasibility of our approach, we integrate our auditing system into OpenStack, one of the most used cloud infrastructure management systems. To show the scalability and validity of our framework, we present our experimental results on assessing several properties related to auditing inter-layer consistency, virtual machines co-residence, and virtual resources isolation.

Madi, Taous, Majumdar, Suryadipta, Wang, Yushun, Jarraya, Yosr, Pourzandi, Makan, Wang, Lingyu.  2016.  Auditing Security Compliance of the Virtualized Infrastructure in the Cloud: Application to OpenStack. Proceedings of the Sixth ACM Conference on Data and Application Security and Privacy. :195–206.

Cloud service providers typically adopt the multi-tenancy model to optimize resources usage and achieve the promised cost-effectiveness. Sharing resources between different tenants and the underlying complex technology increase the necessity of transparency and accountability. In this regard, auditing security compliance of the provider's infrastructure against standards, regulations and customers' policies takes on an increasing importance in the cloud to boost the trust between the stakeholders. However, virtualization and scalability make compliance verification challenging. In this work, we propose an automated framework that allows auditing the cloud infrastructure from the structural point of view while focusing on virtualization-related security properties and consistency between multiple control layers. Furthermore, to show the feasibility of our approach, we integrate our auditing system into OpenStack, one of the most used cloud infrastructure management systems. To show the scalability and validity of our framework, we present our experimental results on assessing several properties related to auditing inter-layer consistency, virtual machines co-residence, and virtual resources isolation.

Dreier, Jannik, Hirschi, Lucca, Radomirovic, Sasa, Sasse, Ralf.  2018.  Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. 2018 IEEE 31st Computer Security Foundations Symposium (CSF). :359-373.

Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. The Tamarin prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes Tamarin the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

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.

Künnemann, Robert, Esiyok, Ilkan, Backes, Michael.  2019.  Automated Verification of Accountability in Security Protocols. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :397—39716.

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 the verification of accountability and demonstrate its use for verification and attack finding on various examples from the accountability and causality literature, including Certificate Transparency and Krollˆ\textbackslashtextbackslashprimes Accountable Algorithms protocol. We reach a high degree of automation by expressing accountability in terms of a set of trace properties and show their soundness and completeness.

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.

Schäfer, Steven, Schneider, Sigurd, Smolka, Gert.  2016.  Axiomatic Semantics for Compiler Verification. Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. :188–196.

Based on constructive type theory, we study two idealized imperative languages GC and IC and verify the correctness of a compiler from GC to IC. GC is a guarded command language with underspecified execution order defined with an axiomatic semantics. IC is a deterministic low-level language with linear sequential composition and lexically scoped gotos defined with a small-step semantics. We characterize IC with an axiomatic semantics and prove that the compiler from GC to IC preserves specifications. The axiomatic semantics we consider model total correctness and map programs to continuous predicate transformers. We define the axiomatic semantics of GC and IC with elementary inductive predicates and show that the predicate transformer described by a program can be obtained compositionally by recursion on the syntax of the program using a fixed point operator for loops and continuations. We also show that two IC programs are contextually equivalent if and only if their predicate transformers are equivalent.

Padon, Oded.  2018.  Deductive Verification of Distributed Protocols in First-Order Logic. 2018 Formal Methods in Computer Aided Design (FMCAD). :1-1.

Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. In the deductive verification approach, the programmer provides inductive invariants and pre/post specifications of procedures, reducing the verification problem to checking validity of logical verification conditions. This check is often performed by automated theorem provers and SMT solvers, substantially increasing productivity in the verification of complex systems. However, the unpredictability of automated provers presents a major hurdle to usability of these tools. This problem is particularly acute in case of provers that handle undecidable logics, for example, first-order logic with quantifiers and theories such as arithmetic. The resulting extreme sensitivity to minor changes has a strong negative impact on the convergence of the overall proof effort.

Sinha, Rohit, Costa, Manuel, Lal, Akash, Lopes, Nuno P., Rajamani, Sriram, Seshia, Sanjit A., Vaswani, Kapil.  2016.  A Design and Verification Methodology for Secure Isolated Regions. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. :665–681.

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running in a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime that implements the narrow interface. The runtime includes services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime's internal state. We present /CONFIDENTIAL: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

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.

Canetti, Ran, Stoughton, Alley, Varia, Mayank.  2019.  EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :167–16716.

We present a methodology for using the EasyCrypt proof assistant (originally designed for mechanizing the generation of proofs of game-based security of cryptographic schemes and protocols) to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework. This allows, for the first time, the mechanization and formal verification of the entire sequence of steps needed for proving simulation-based security in a modular way: Specifying a protocol and the desired ideal functionality; Constructing a simulator and demonstrating its validity, via reduction to hard computational problems; Invoking the universal composition operation and demonstrating that it indeed preserves security. We demonstrate our methodology on a simple example: stating and proving the security of secure message communication via a one-time pad, where the key comes from a Diffie-Hellman key-exchange, assuming ideally authenticated communication. We first put together EasyCrypt-verified proofs that: (a) the Diffie-Hellman protocol UC-realizes an ideal key-exchange functionality, assuming hardness of the Decisional Diffie-Hellman problem, and (b) one-time-pad encryption, with a key obtained using ideal key-exchange, UC-realizes an ideal secure-communication functionality. We then mechanically combine the two proofs into an EasyCrypt-verified proof that the composed protocol realizes the same ideal secure-communication functionality. Although formulating a methodology that is both sound and workable has proven to be a complex task, we are hopeful that it will prove to be the basis for mechanized UC security analyses for significantly more complex protocols and tasks.

Shu-fen, NIU, Bo-bin, WANG, You-chen, WANG, Jin-feng, WANG, Jing-min, CHEN.  2019.  Efficient and Secure Proxy re-signature Message Authentication Scheme in Vehicular Ad Hoc Network. 2019 IEEE 3rd Advanced Information Management, Communicates, Electronic and Automation Control Conference (IMCEC). :1652–1656.

In order to solve privacy protection problem in the Internet of Vehicles environment, a message authentication scheme based on proxy re-signature is proposed using elliptic curves, which realizes privacy protection by transforming the vehicle's signature of the message into the roadside unit's signature of the same message through the trusted center. And through the trusted center traceability, to achieve the condition of privacy protection, and the use of batch verification technology, greatly improve the efficiency of authentication. It is proved that the scheme satisfies unforgeability in ECDLP hard problem in the random oracle model. The efficiency analysis shows that the scheme meets the security and efficiency requirements of the Internet of Vehicles and has certain practical significance.

Puccetti, Armand.  2019.  The European H2020 project VESSEDIA (Verification Engineering of Safety and SEcurity critical Dynamic Industrial Applications). 2019 22nd Euromicro Conference on Digital System Design (DSD). :588—591.

This paper presents an overview of the H2020 project VESSEDIA [9] aimed at verifying the security and safety of modern connected systems also called IoT. The originality relies in using Formal Methods inherited from high-criticality applications domains to analyze the source code at different levels of intensity, to gather possible faults and weaknesses. The analysis methods are mostly exhaustive an guarantee that, after analysis, the source code of the application is error-free. This paper is structured as follows: after an introductory section 1 giving some factual data, section 2 presents the aims and the problems addressed; section 3 describes the project's use-cases and section 4 describes the proposed approach for solving these problems and the results achieved until now; finally, section 5 discusses some remaining future work.