Visible to the public Biblio

Found 123 results

Filters: Keyword is formal verification  [Clear All Filters]
2021-07-08
SAMMOUD, Amal, CHALOUF, Mohamed Aymen, HAMDI, Omessaad, MONTAVONT, Nicolas, Bouallègue, Ammar.  2020.  A secure and lightweight three-factor authentication and key generation scheme for direct communication between healthcare professionals and patient’s WMSN. 2020 IEEE Symposium on Computers and Communications (ISCC). :1—6.
One of the main security issues in telecare medecine information systems is the remote user authentication and key agreement between healthcare professionals and patient's medical sensors. Many of the proposed approaches are based on multiple factors (password, token and possibly biometrics). Two-factor authentication protocols do not resist to many possible attacks. As for three-factor authentication schemes, they usually come with high resource consumption. Since medical sensors have limited storage and computational capabilities, ensuring a minimal resources consumption becomes a major concern in this context. In this paper, we propose a secure and lightweight three-factor authentication and key generation scheme for securing communications between healtcare professional and patient's medical sensors. Thanks to formal verification, we prove that this scheme is robust enough against known possible attacks. A comparison with the most relevant related work's schemes shows that our protocol ensures an optimised resource consumption level.
2021-05-13
Sardar, Muhammad Usama, Quoc, Do Le, Fetzer, Christof.  2020.  Towards Formalization of Enhanced Privacy ID (EPID)-based Remote Attestation in Intel SGX. 2020 23rd Euromicro Conference on Digital System Design (DSD). :604—607.

Vulnerabilities in privileged software layers have been exploited with severe consequences. Recently, Trusted Execution Environments (TEEs) based technologies have emerged as a promising approach since they claim strong confidentiality and integrity guarantees regardless of the trustworthiness of the underlying system software. In this paper, we consider one of the most prominent TEE technologies, referred to as Intel Software Guard Extensions (SGX). Despite many formal approaches, there is still a lack of formal proof of some critical processes of Intel SGX, such as remote attestation. To fill this gap, we propose a fully automated, rigorous, and sound formal approach to specify and verify the Enhanced Privacy ID (EPID)-based remote attestation in Intel SGX under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. The evaluation indicates that the confidentiality of attestation keys is preserved against a Dolev-Yao adversary in this technology. We also present a few of the many inconsistencies found in the existing literature on Intel SGX attestation during formal specification.

2021-05-03
Le, Son N., Srinivasan, Sudarshan K., Smith, Scott C..  2020.  Exploiting Dual-Rail Register Invariants for Equivalence Verification of NCL Circuits. 2020 IEEE 63rd International Midwest Symposium on Circuits and Systems (MWSCAS). :21–24.
Equivalence checking is one of the most scalable and useful verification techniques in industry. NULL Convention Logic (NCL) circuits utilize dual-rail signals (i.e., two wires to represent one bit of DATA), where the wires are inverses of each other during a DATA wavefront. In this paper, a technique that exploits this invariant at NCL register boundaries is proposed to improve the efficiency of equivalence verification of NCL circuits.
2021-03-18
Baolin, X., Minhuan, Z..  2020.  A Solution of Text Based CAPTCHA without Network Flow Consumption. 2020 IEEE 11th International Conference on Software Engineering and Service Science (ICSESS). :395—399.

With the widespread application of distributed information processing, information processing security issues have become one of the important research topics; CAPTCHA technology is often used as the first security barrier for distributed information processing and it prevents the client malicious programs to attack the server. The experiment proves that the existing “request / response” mode of CAPTCHA has great security risks. “The text-based CAPTCHA solution without network flow consumption” proposed in this paper avoids the “request / response” mode and the verification logic of the text-based CAPTCHA is migrated to the client in this solution, which fundamentally cuts off the client's attack facing to the server during the verification of the CAPTCHA and it is a high-security text-based CAPTCHA solution without network flow consumption.

2021-02-16
Kang, E., Schobbens, P..  2020.  InFoCPS: Integrating Formal Analysis of Cyber-Physical Systems with Energy Prognostics. 2020 9th Mediterranean Conference on Embedded Computing (MECO). :1—5.
This paper is related to dissemination and exploitation of the InFoCPS PhD research project: Failure of Cyber-Physical Systems (CPS) may cause extensive damage. Safety standards emphasize the use of formal analysis in CPS development processes. Performance degradation assessment and estimation of lifetime of energy storage (electric batteries) are vital in supporting maintenance decisions and guaranteeing CPS reliability. Existing formal analysis techniques mainly focus on specifying energy constraints in simplified manners and checking whether systems operate within given energy bounds. Leading to overlooked energy features that impede development of trustworthy CPS. Prognostics and health management (PHM) estimate energy uncertainty and predict remaining life of systems. We aim to utilize PHM techniques to rigorously model dynamic energy behaviors; resulting models are amenable to formal analysis. This project will increase the degree of maintenance of CPS while (non)-functional requirements are preserved correctly.
2021-01-28
Sammoud, A., Chalouf, M. A., Hamdi, O., Montavont, N., Bouallegue, A..  2020.  A secure three-factor authentication and biometrics-based key agreement scheme for TMIS with user anonymity. 2020 International Wireless Communications and Mobile Computing (IWCMC). :1916—1921.

E- Health systems, specifically, Telecare Medical Information Systems (TMIS), are deployed in order to provide patients with specific diseases with healthcare services that are usually based on remote monitoring. Therefore, making an efficient, convenient and secure connection between users and medical servers over insecure channels within medical services is a rather major issue. In this context, because of the biometrics' characteristics, many biometrics-based three factor user authentication schemes have been proposed in the literature to secure user/server communication within medical services. In this paper, we make a brief study of the most interesting proposals. Then, we propose a new three-factor authentication and key agreement scheme for TMIS. Our scheme tends not only to fix the security drawbacks of some studied related work, but also, offers additional significant features while minimizing resource consumption. In addition, we perform a formal verification using the widely accepted formal security verification tool AVISPA to demonstrate that our proposed scheme is secure. Also, our comparative performance analysis reveals that our proposed scheme provides a lower resource consumption compared to other related work's proposals.

2021-01-25
Ghazo, A. T. Al, Ibrahim, M., Ren, H., Kumar, R..  2020.  A2G2V: Automatic Attack Graph Generation and Visualization and Its Applications to Computer and SCADA Networks. IEEE Transactions on Systems, Man, and Cybernetics: Systems. 50:3488–3498.
Securing cyber-physical systems (CPS) and Internet of Things (IoT) systems requires the identification of how interdependence among existing atomic vulnerabilities may be exploited by an adversary to stitch together an attack that can compromise the system. Therefore, accurate attack graphs play a significant role in systems security. A manual construction of the attack graphs is tedious and error-prone, this paper proposes a model-checking-based automated attack graph generator and visualizer (A2G2V). The proposed A2G2V algorithm uses existing model-checking tools, an architecture description tool, and our own code to generate an attack graph that enumerates the set of all possible sequences in which atomic-level vulnerabilities can be exploited to compromise system security. The architecture description tool captures a formal representation of the networked system, its atomic vulnerabilities, their pre-and post-conditions, and security property of interest. A model-checker is employed to automatically identify an attack sequence in the form of a counterexample. Our own code integrated with the model-checker parses the counterexamples, encodes those for specification relaxation, and iterates until all attack sequences are revealed. Finally, a visualization tool has also been incorporated with A2G2V to generate a graphical representation of the generated attack graph. The results are illustrated through application to computer as well as control (SCADA) networks.
2021-01-20
Li, Y., Yang, Y., Yu, X., Yang, T., Dong, L., Wang, W..  2020.  IoT-APIScanner: Detecting API Unauthorized Access Vulnerabilities of IoT Platform. 2020 29th International Conference on Computer Communications and Networks (ICCCN). :1—5.

The Internet of Things enables interaction between IoT devices and users through the cloud. The cloud provides services such as account monitoring, device management, and device control. As the center of the IoT platform, the cloud provides services to IoT devices and IoT applications through APIs. Therefore, the permission verification of the API is essential. However, we found that some APIs are unverified, which allows unauthorized users to access cloud resources or control devices; it could threaten the security of devices and cloud. To check for unauthorized access to the API, we developed IoT-APIScanner, a framework to check the permission verification of the cloud API. Through observation, we found there is a large amount of interactive information between IoT application and cloud, which include the APIs and related parameters, so we can extract them by analyzing the code of the IoT application, and use this for mutating API test cases. Through these test cases, we can effectively check the permissions of the API. In our research, we extracted a total of 5 platform APIs. Among them, the proportion of APIs without permission verification reached 13.3%. Our research shows that attackers could use the API without permission verification to obtain user privacy or control of devices.

Atlidakis, V., Godefroid, P., Polishchuk, M..  2020.  Checking Security Properties of Cloud Service REST APIs. 2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST). :387—397.

Most modern cloud and web services are programmatically accessed through REST APIs. This paper discusses how an attacker might compromise a service by exploiting vulnerabilities in its REST API. We introduce four security rules that capture desirable properties of REST APIs and services. We then show how a stateful REST API fuzzer can be extended with active property checkers that automatically test and detect violations of these rules. We discuss how to implement such checkers in a modular and efficient way. Using these checkers, we found new bugs in several deployed production Azure and Office365 cloud services, and we discuss their security implications. All these bugs have been fixed.

2020-12-07
Whitefield, J., Chen, L., Sasse, R., Schneider, S., Treharne, H., Wesemeyer, S..  2019.  A Symbolic Analysis of ECC-Based Direct Anonymous Attestation. 2019 IEEE European Symposium on Security and Privacy (EuroS P). :127–141.
Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module TPM-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol's expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.
2020-11-09
Ya'u, B. I., Nordin, A., Salleh, N., Aliyu, I..  2018.  Requirements Patterns Structure for Specifying and Reusing Software Product Line Requirements. 2018 International Conference on Information and Communication Technology for the Muslim World (ICT4M). :185–190.
A well-defined structure is essential in all software development, thus providing an avenue for smooth execution of the processes involved during various software development phases. One of the potential benefits provided by a well-defined structure is systematic reuse of software artifacts. Requirements pattern approach provides guidelines and modality that enables a systematic way of specifying and documenting requirements, which in turn supports a systematic reuse. Although there is a great deal of research concerning requirements pattern in the literature, the research focuses are not on requirement engineering (RE) activities of SPLE. In this paper, we proposed a software requirement pattern (SRP) structure based on RePa Requirements Pattern Template, which was adapted to best suit RE activities in SPLE. With this requirement pattern structure, RE activities such as elicitation and identification of common and variable requirements as well as the specification, documentation, and reuse in SPLE could be substantially improved.
2020-11-04
Zong, P., Wang, Y., Xie, F..  2018.  Embedded Software Fault Prediction Based on Back Propagation Neural Network. 2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :553—558.

Predicting software faults before software testing activities can help rational distribution of time and resources. Software metrics are used for software fault prediction due to their close relationship with software faults. Thanks to the non-linear fitting ability, Neural networks are increasingly used in the prediction model. We first filter metric set of the embedded software by statistical methods to reduce the dimensions of model input. Then we build a back propagation neural network with simple structure but good performance and apply it to two practical embedded software projects. The verification results show that the model has good ability to predict software faults.

2020-11-02
Qin, Maoyuan, Hu, Wei, Mu, Dejun, Tai, Yu.  2018.  Property Based Formal Security Verification for Hardware Trojan Detection. 2018 IEEE 3rd International Verification and Security Workshop (IVSW). :62—67.

The design of modern computer hardware heavily relies on third-party intellectual property (IP) cores, which may contain malicious hardware Trojans that could be exploited by an adversary to leak secret information or take control of the system. Existing hardware Trojan detection methods either require a golden reference design for comparison or extensive functional testing to identify suspicious signals. In this paper, we propose a new formal verification method to verify the security of hardware designs. The proposed solution formalizes fine grained gate level information flow model for proving security properties of hardware designs in the Coq theorem prover environment. Compare with existing register transfer level (RTL) information flow security models, our model only needs to translate a small number of logic primitives to their formal representations without the need of supporting the rich RTL HDL semantics or dealing with complex conditional branch or loop structures. As a result, a gate level information flow model can be created at much lower complexity while achieving significantly higher precision in modeling the security behavior of hardware designs. We use the AES-T1700 benchmark from Trust-HUB to demonstrate the effectiveness of our solution. Experimental results show that our method can detect and pinpoint the Trojan.

2020-10-26
Criswell, John, Zhou, Jie, Gravani, Spyridoula, Hu, Xiaoyu.  2019.  PrivAnalyzer: Measuring the Efficacy of Linux Privilege Use. 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). :593–604.
Operating systems such as Linux break the power of the root user into separate privileges (which Linux calls capabilities) and give processes the ability to enable privileges only when needed and to discard them permanently when the program no longer needs them. However, there is no method of measuring how well the use of such facilities reduces the risk of privilege escalation attacks if the program has a vulnerability. This paper presents PrivAnalyzer, an automated tool that measures how effectively programs use Linux privileges. PrivAnalyzer consists of three components: 1) AutoPriv, an existing LLVM-based C/C++ compiler which uses static analysis to transform a program that uses Linux privileges into a program that safely removes them when no longer needed, 2) ChronoPriv, a new LLVM C/C++ compiler pass that performs dynamic analysis to determine for how long a program retains various privileges, and 3) ROSA, a new bounded model checker that can model the damage a program can do at each program point if an attacker can exploit the program and abuse its privileges. We use PrivAnalyzer to determine how long five privileged open source programs retain the ability to cause serious damage to a system and find that merely transforming a program to drop privileges does not significantly improve security. However, we find that simple refactoring can considerably increase the efficacy of Linux privileges. In two programs that we refactored, we reduced the percentage of execution in which a device file can be read and written from 97% and 88% to 4% and 1%, respectively.
2020-10-16
Babenko, Liudmila, Pisarev, Ilya.  2018.  Security Analysis of the Electronic Voting Protocol Based on Blind Intermediaries Using the SPIN Verifier. 2018 International Conference on Cyber-Enabled Distributed Computing and Knowledge Discovery (CyberC). :43—435.

Cryptographic protocols are the basis for the security of any protected system, including the electronic voting system. One of the most effective ways to analyze protocol security is to use verifiers. In this paper, the formal verifier SPIN was used to analyze the security of the cryptographic protocol for e-voting, which is based on model checking using linear temporal logic (LTL). The cryptographic protocol of electronic voting is described. The main structural units of the Promela language used for simulation in the SPIN verifier are described. The model of the electronic voting protocol in the language Promela is given. The interacting parties, transferred data, the order of the messages transmitted between the parties are described. Security of the cryptographic protocol using the SPIN tool is verified. The simulation of the protocol with active intruder using the man in the middle attack (MITM) to substitute data is made. In the simulation results it is established that the protocol correctly handles the case of an active attack on the parties' authentication.

2020-10-06
André, Étienne, Lime, Didier, Ramparison, Mathias, Stoelinga, Mariëlle.  2019.  Parametric Analyses of Attack-Fault Trees. 2019 19th International Conference on Application of Concurrency to System Design (ACSD). :33—42.

Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e., absence of unintentional failures) and security (i. e., no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to help considering these problems is attack trees, a tree-based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parametrize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure.

2020-09-28
Simos, Dimitris E., Garn, Bernhard, Zivanovic, Jovan, Leithner, Manuel.  2019.  Practical Combinatorial Testing for XSS Detection using Locally Optimized Attack Models. 2019 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). :122–130.
In this paper, we present a combinatorial testing methodology for automated black-box security testing of complex web applications. The focus of our work is the identification of Cross-site Scripting (XSS) vulnerabilities. We introduce a new modelling scheme for test case generation of XSS attack vectors consisting of locally optimized attack models. The modelling approach takes into account the response and behavior of the web application and is particularly efficient when used in conjunction with combinatorial testing. In addition to the modelling scheme, we present a research prototype of a security testing tool called XSSInjector, which executes attack vectors generated from our methodology against web applications. The tool also employs a newly developed test oracle for detecting XSS which allow us to precisely identify whether injected JavaScript is actually executed and thus eliminate false positives. Our testing methodology is sufficiently generic to be applied to any web application that returns HTML code. We describe the foundations of our approach and validate it via an extensive case study using a verification framework and real world web applications. In particular, we have found several new critical vulnerabilities in popular forum software, library management systems and gallery packages.
Chen, Yuqi, Poskitt, Christopher M., Sun, Jun.  2018.  Learning from Mutants: Using Code Mutation to Learn and Monitor Invariants of a Cyber-Physical System. 2018 IEEE Symposium on Security and Privacy (SP). :648–660.
Cyber-physical systems (CPS) consist of sensors, actuators, and controllers all communicating over a network; if any subset becomes compromised, an attacker could cause significant damage. With access to data logs and a model of the CPS, the physical effects of an attack could potentially be detected before any damage is done. Manually building a model that is accurate enough in practice, however, is extremely difficult. In this paper, we propose a novel approach for constructing models of CPS automatically, by applying supervised machine learning to data traces obtained after systematically seeding their software components with faults ("mutants"). We demonstrate the efficacy of this approach on the simulator of a real-world water purification plant, presenting a framework that automatically generates mutants, collects data traces, and learns an SVM-based model. Using cross-validation and statistical model checking, we show that the learnt model characterises an invariant physical property of the system. Furthermore, we demonstrate the usefulness of the invariant by subjecting the system to 55 network and code-modification attacks, and showing that it can detect 85% of them from the data logs generated at runtime.
2020-09-18
Guo, Xiaolong, Dutta, Raj Gautam, He, Jiaji, Tehranipoor, Mark M., Jin, Yier.  2019.  QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment. 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). :91—100.
Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issue. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically, and that our method evaluates the security of the design correctly.
2020-09-14
Lochbihler, Andreas, Sefidgar, S. Reza, Basin, David, Maurer, Ueli.  2019.  Formalizing Constructive Cryptography using CryptHOL. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :152–15214.
Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Existing tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composability have met with limited success. In this paper, we formalize an instance of Constructive Cryptography, a generic theory allowing for clean, composable cryptographic security statements. Namely, we extend CryptHOL, a framework for game-based proofs, with an abstract model of Random Systems and provide proof rules for their equality and composition. We formalize security as a special kind of system construction in which a complex system is built from simpler ones. As a simple case study, we formalize the construction of an information-theoretically secure channel from a key, a random function, and an insecure channel.
2020-09-04
Elkanishy, Abdelrahman, Badawy, Abdel-Hameed A., Furth, Paul M., Boucheron, Laura E., Michael, Christopher P..  2019.  Machine Learning Bluetooth Profile Operation Verification via Monitoring the Transmission Pattern. 2019 53rd Asilomar Conference on Signals, Systems, and Computers. :2144—2148.
Manufacturers often buy and/or license communication ICs from third-party suppliers. These communication ICs are then integrated into a complex computational system, resulting in a wide range of potential hardware-software security issues. This work proposes a compact supervisory circuit to classify the Bluetooth profile operation of a Bluetooth System-on-Chip (SoC) at low frequencies by monitoring the radio frequency (RF) output power of the Bluetooth SoC. The idea is to inexpensively manufacture an RF envelope detector to monitor the RF output power and a profile classification algorithm on a custom low-frequency integrated circuit in a low-cost legacy technology. When the supervisory circuit observes unexpected behavior, it can shut off power to the Bluetooth SoC. In this preliminary work, we proto-type the supervisory circuit using off-the-shelf components to collect a sufficient data set to train 11 different Machine Learning models. We extract smart descriptive time-domain features from the envelope of the RF output signal. Then, we train the machine learning models to classify three different Bluetooth operation profiles: sensor, hands-free, and headset. Our results demonstrate 100% classification accuracy with low computational complexity.
2020-08-03
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.

2020-07-24
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.
2020-07-16
Yuan, Haoxuan, Li, Fang, Huang, Xin.  2019.  A Formal Modeling and Verification Framework for Service Oriented Intelligent Production Line Design. 2019 IEEE/ACIS 18th International Conference on Computer and Information Science (ICIS). :173—178.

The intelligent production line is a complex application with a large number of independent equipment network integration. In view of the characteristics of CPS, the existing modeling methods cannot well meet the application requirements of large scale high-performance system. a formal simulation verification framework and verification method are designed for the performance constraints such as the real-time and security of the intelligent production line based on soft bus. A model-based service-oriented integration approach is employed, which adopts a model-centric way to automate the development course of the entire software life cycle. Developing experience indicate that the proposed approach based on the formal modeling and verification framework in this paper can improve the performance of the system, which is also helpful to achieve the balance of the production line and maintain the reasonable use rate of the processing equipment.

2020-07-10
Zhang, Mengyu, Zhang, Hecan, Yang, Yahui, Shen, Qingni.  2019.  PTAD:Provable and Traceable Assured Deletion in Cloud Storage. 2019 IEEE Symposium on Computers and Communications (ISCC). :1—6.

As an efficient deletion method, unlinking is widely used in cloud storage. While unlinking is a kind of incomplete deletion, `deleted data' remains on cloud and can be recovered. To make `deleted data' unrecoverable, overwriting is an effective method on cloud. Users lose control over their data on cloud once deleted, so it is difficult for them to confirm overwriting. In face of such a crucial problem, we propose a Provable and Traceable Assured Deletion (PTAD) scheme in cloud storage based on blockchain. PTAD scheme relies on overwriting to achieve assured deletion. We reference the idea of data integrity checking and design algorithms to verify if cloud overwrites original blocks properly as specific patterns. We utilize technique of smart contract in blockchain to automatically execute verification and keep transaction in ledger for tracking. The whole scheme can be divided into three stages-unlinking, overwriting and verification-and we design one specific algorithm for each stage. For evaluation, we implement PTAD scheme on cloud and construct a consortium chain with Hyperledger Fabric. The performance shows that PTAD scheme is effective and feasible.