Visible to the public Biblio

Found 411 results

Filters: Keyword is Analytical models  [Clear All Filters]
2020-05-04
Rauscher, Julia, Bauer, Bernhard.  2018.  Safety and Security Architecture Analyses Framework for the Internet of Things of Medical Devices. 2018 IEEE 20th International Conference on e-Health Networking, Applications and Services (Healthcom). :1–3.
Internet of Things (IoT) is spreading increasingly in different areas of application. Accordingly, IoT also gets deployed in health care including ambient assisted living, telemedicine or medical smart homes. However, IoT also involves risks. Next to increased security issues also safety concerns are occurring. Deploying health care sensors and utilizing medical data causes a high need for IoT architectures free of vulnerabilities in order to identify weak points as early as possible. To address this, we are developing a safety and security analysis approach including a standardized meta model and an IoT safety and security framework comprising a customizable analysis language.
2020-04-20
Khan, Muhammad Imran, Foley, Simon N., O'Sullivan, Barry.  2019.  PriDe: A Quantitative Measure of Privacy-Loss in Interactive Querying Settings. 2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS). :1–5.
This paper presents, PriDe, a model to measure the deviation of an analyst's (user) querying behaviour from normal querying behaviour. The deviation is measured in terms of privacy, that is to say, how much of the privacy loss has incurred due to this shift in querying behaviour. The shift is represented in terms of a score - a privacy-loss score, the higher the score the more the loss in privacy. Querying behaviour of analysts are modelled using n-grams of SQL query and subsequently, behavioural profiles are constructed. Profiles are then compared in terms of privacy resulting in a quantified score indicating the privacy loss.
To, Hien, Shahabi, Cyrus, Xiong, Li.  2018.  Privacy-Preserving Online Task Assignment in Spatial Crowdsourcing with Untrusted Server. 2018 IEEE 34th International Conference on Data Engineering (ICDE). :833–844.
With spatial crowdsourcing (SC), requesters outsource their spatiotemporal tasks (tasks associated with location and time) to a set of workers, who will perform the tasks by physically traveling to the tasks' locations. However, current solutions require the locations of the workers and/or the tasks to be disclosed to untrusted parties (SC server) for effective assignments of tasks to workers. In this paper we propose a framework for assigning tasks to workers in an online manner without compromising the location privacy of workers and tasks. We perturb the locations of both tasks and workers based on geo-indistinguishability and then devise techniques to quantify the probability of reachability between a task and a worker, given their perturbed locations. We investigate both analytical and empirical models for quantifying the worker-task pair reachability and propose task assignment strategies that strike a balance among various metrics such as the number of completed tasks, worker travel distance and system overhead. Extensive experiments on real-world datasets show that our proposed techniques result in minimal disclosure of task locations and no disclosure of worker locations without significantly sacrificing the total number of assigned tasks.
To, Hien, Shahabi, Cyrus, Xiong, Li.  2018.  Privacy-Preserving Online Task Assignment in Spatial Crowdsourcing with Untrusted Server. 2018 IEEE 34th International Conference on Data Engineering (ICDE). :833–844.
With spatial crowdsourcing (SC), requesters outsource their spatiotemporal tasks (tasks associated with location and time) to a set of workers, who will perform the tasks by physically traveling to the tasks' locations. However, current solutions require the locations of the workers and/or the tasks to be disclosed to untrusted parties (SC server) for effective assignments of tasks to workers. In this paper we propose a framework for assigning tasks to workers in an online manner without compromising the location privacy of workers and tasks. We perturb the locations of both tasks and workers based on geo-indistinguishability and then devise techniques to quantify the probability of reachability between a task and a worker, given their perturbed locations. We investigate both analytical and empirical models for quantifying the worker-task pair reachability and propose task assignment strategies that strike a balance among various metrics such as the number of completed tasks, worker travel distance and system overhead. Extensive experiments on real-world datasets show that our proposed techniques result in minimal disclosure of task locations and no disclosure of worker locations without significantly sacrificing the total number of assigned tasks.
2020-04-06
Liu, Lan, Lin, Jun, Wang, Qiang, Xu, Xiaoping.  2018.  Research on Network Malicious Code Detection and Provenance Tracking in Future Network. 2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :264–268.
with the development of SDN, ICN and 5G networks, the research of future network becomes a hot topic. Based on the design idea of SDN network, this paper analyzes the propagation model and detection method of malicious code in future network. We select characteristics of SDN and analyze the features use different feature selection methods and sort the features. After comparison the influence of running time by different classification algorithm of different feature selection, we analyze the choice of reduction dimension m, and find out the different types of malicious code corresponding to the optimal feature subset and matching classification method, designed for malware detection system. We analyze the node migration rate of malware in mobile network and its effect on the outbreak of the time. In this way, it can provide reference for the management strategy of the switch node or the host node by future network controller.
2020-04-03
Aires Urquiza, Abraão, AlTurki, Musab A., Kanovich, Max, Ban Kirigin, Tajana, Nigam, Vivek, Scedrov, Andre, Talcott, Carolyn.  2019.  Resource-Bounded Intruders in Denial of Service Attacks. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :382—38214.

Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. This paper proposes a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. In contrast to the existing resource-conscious protocol verification models, our model allows finer and more subtle analysis of DoS problems. We illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Finally, we implemented our formal verification model in the rewriting logic tool Maude and analyzed a number of DoS attacks in Maude using Rewriting Modulo SMT in an automated fashion.

2020-03-16
Singh, Rina, Graves, Jeffrey A., Anantharaj, Valentine, Sukumar, Sreenivas R..  2019.  Evaluating Scientific Workflow Engines for Data and Compute Intensive Discoveries. 2019 IEEE International Conference on Big Data (Big Data). :4553–4560.
Workflow engines used to script scientific experiments involving numerical simulation, data analysis, instruments, edge sensors, and artificial intelligence have to deal with the complexities of hardware, software, resource availability, and the collaborative nature of science. In this paper, we survey workflow engines used in data-intensive and compute-intensive discovery pipelines from scientific disciplines such as astronomy, high energy physics, earth system science, bio-medicine, and material science and present a qualitative analysis of their respective capabilities. We compare 5 popular workflow engines and their differentiated approach to job orchestration, job launching, data management and provenance, security authentication, ease-ofuse, workflow description, and scripting semantics. The comparisons presented in this paper allow practitioners to choose the appropriate engine for their scientific experiment and lead to recommendations for future work.
2020-03-09
Sion, Laurens, Van Landuyt, Dimitri, Wuyts, Kim, Joosen, Wouter.  2019.  Privacy Risk Assessment for Data Subject-Aware Threat Modeling. 2019 IEEE Security and Privacy Workshops (SPW). :64–71.
Regulatory efforts such as the General Data Protection Regulation (GDPR) embody a notion of privacy risk that is centered around the fundamental rights of data subjects. This is, however, a fundamentally different notion of privacy risk than the one commonly used in threat modeling which is largely agnostic of involved data subjects. This mismatch hampers the applicability of privacy threat modeling approaches such as LINDDUN in a Data Protection by Design (DPbD) context. In this paper, we present a data subject-aware privacy risk assessment model in specific support of privacy threat modeling activities. This model allows the threat modeler to draw upon a more holistic understanding of privacy risk while assessing the relevance of specific privacy threats to the system under design. Additionally, we propose a number of improvements to privacy threat modeling, such as enriching Data Flow Diagram (DFD) system models with appropriate risk inputs (e.g., information on data types and involved data subjects). Incorporation of these risk inputs in DFDs, in combination with a risk estimation approach using Monte Carlo simulations, leads to a more comprehensive assessment of privacy risk. The proposed risk model has been integrated in threat modeling tool prototype and validated in the context of a realistic eHealth application.
2020-02-26
Sabbagh, Majid, Gongye, Cheng, Fei, Yunsi, Wang, Yanzhi.  2019.  Evaluating Fault Resiliency of Compressed Deep Neural Networks. 2019 IEEE International Conference on Embedded Software and Systems (ICESS). :1–7.

Model compression is considered to be an effective way to reduce the implementation cost of deep neural networks (DNNs) while maintaining the inference accuracy. Many recent studies have developed efficient model compression algorithms and implementations in accelerators on various devices. Protecting integrity of DNN inference against fault attacks is important for diverse deep learning enabled applications. However, there has been little research investigating the fault resilience of DNNs and the impact of model compression on fault tolerance. In this work, we consider faults on different data types and develop a simulation framework for understanding the fault resiliency of compressed DNN models as compared to uncompressed models. We perform our experiments on two common DNNs, LeNet-5 and VGG16, and evaluate their fault resiliency with different types of compression. The results show that binary quantization can effectively increase the fault resilience of DNN models by 10000x for both LeNet5 and VGG16. Finally, we propose software and hardware mitigation techniques to increase the fault resiliency of DNN models.

2020-02-18
Zheng, Jianjun, Siami Namin, Akbar.  2019.  Enforcing Optimal Moving Target Defense Policies. 2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC). 1:753–759.
This paper introduces an approach based on control theory to model, analyze and select optimal security policies for Moving Target Defense (MTD) deployment strategies. A Markov Decision Process (MDP) scheme is presented to model states of the system from attacking point of view. The employed value iteration method is based on the Bellman optimality equation for optimal policy selection for each state defined in the system. The model is then utilized to analyze the impact of various costs on the optimal policy. The MDP model is then applied to two case studies to evaluate the performance of the model.
Dishington, Cole, Sharma, Dilli P., Kim, Dong Seong, Cho, Jin-Hee, Moore, Terrence J., Nelson, Frederica F..  2019.  Security and Performance Assessment of IP Multiplexing Moving Target Defence in Software Defined Networks. 2019 18th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/13th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :288–295.

With the interconnection of services and customers, network attacks are capable of large amounts of damage. Flexible Random Virtual IP Multiplexing (FRVM) is a Moving Target Defence (MTD) technique that protects against reconnaissance and access with address mutation and multiplexing. Security techniques must be trusted, however, FRVM, along with past MTD techniques, have gaps in realistic evaluation and thorough analysis of security and performance. FRVM, and two comparison techniques, were deployed on a virtualised network to demonstrate FRVM's security and performance trade-offs. The key results include the security and performance trade-offs of address multiplexing and address mutation. The security benefit of IP address multiplexing is much greater than its performance overhead, deployed on top of address mutation. Frequent address mutation significantly increases an attackers' network scan durations as well as effectively obfuscating and hiding network configurations.

2020-02-17
Yin, Mingyong, Wang, Qixu, Cao, Mingsheng.  2019.  An Attack Vector Evaluation Method for Smart City Security Protection. 2019 International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob). :1–7.

In the network security risk assessment on critical information infrastructure of smart city, to describe attack vectors for predicting possible initial access is a challenging task. In this paper, an attack vector evaluation model based on weakness, path and action is proposed, and the formal representation and quantitative evaluation method are given. This method can support the assessment of attack vectors based on known and unknown weakness through combination of depend conditions. In addition, defense factors are also introduced, an attack vector evaluation model of integrated defense is proposed, and an application example of the model is given. The research work in this paper can provide a reference for the vulnerability assessment of attack vector.

Fett, Daniel, Hosseyni, Pedram, Küsters, Ralf.  2019.  An Extensive Formal Security Analysis of the OpenID Financial-Grade API. 2019 IEEE Symposium on Security and Privacy (SP). :453–471.
Forced by regulations and industry demand, banks worldwide are working to open their customers' online banking accounts to third-party services via web-based APIs. By using these so-called Open Banking APIs, third-party companies, such as FinTechs, are able to read information about and initiate payments from their users' bank accounts. Such access to financial data and resources needs to meet particularly high security requirements to protect customers. One of the most promising standards in this segment is the OpenID Financial-grade API (FAPI), currently under development in an open process by the OpenID Foundation and backed by large industry partners. The FAPI is a profile of OAuth 2.0 designed for high-risk scenarios and aiming to be secure against very strong attackers. To achieve this level of security, the FAPI employs a range of mechanisms that have been developed to harden OAuth 2.0, such as Code and Token Binding (including mTLS and OAUTB), JWS Client Assertions, and Proof Key for Code Exchange. In this paper, we perform a rigorous, systematic formal analysis of the security of the FAPI, based on an existing comprehensive model of the web infrastructure - the Web Infrastructure Model (WIM) proposed by Fett, Küsters, and Schmitz. To this end, we first develop a precise model of the FAPI in the WIM, including different profiles for read-only and read-write access, different flows, different types of clients, and different combinations of security features, capturing the complex interactions in a web-based environment. We then use our model of the FAPI to precisely define central security properties. In an attempt to prove these properties, we uncover partly severe attacks, breaking authentication, authorization, and session integrity properties. We develop mitigations against these attacks and finally are able to formally prove the security of a fixed version of the FAPI. Although financial applications are high-stakes environments, this work is the first to formally analyze and, importantly, verify an Open Banking security profile. By itself, this analysis is an important contribution to the development of the FAPI since it helps to define exact security properties and attacker models, and to avoid severe security risks before the first implementations of the standard go live. Of independent interest, we also uncover weaknesses in the aforementioned security mechanisms for hardening OAuth 2.0. We illustrate that these mechanisms do not necessarily achieve the security properties they have been designed for.
Biswal, Satya Ranjan, Swain, Santosh Kumar.  2019.  Model for Study of Malware Propagation Dynamics in Wireless Sensor Network. 2019 3rd International Conference on Trends in Electronics and Informatics (ICOEI). :647–653.
Wireless Sensor Network (WSN) faces critical security challenges due to malware(worm, virus, malicious code etc.) attack. When a single node gets compromised by malware then start to spread in entire sensor network through neighboring sensor nodes. To understand the dynamics of malware propagation in WSN proposed a Susceptible-Exposed-Infectious-Recovered-Dead (SEIRD) model. This model used the concept of epidemiology. The model focused on early detection of malicious signals presence in the network and accordingly application of security mechanism for its removal. The early detection method helps in controlling of malware spread and reduce battery consumption of sensor nodes. In this paper study the dynamics of malware propagation and stability analysis of the system. In epidemiology basic reproduction number is a crucial parameter which is used for the determination of malware status in the system. The expression of basic reproduction number has been obtained. Analyze the propagation dynamics and compared with previous model. The proposed model provides improved security mechanism in comparison to previous one. The extensive simulation results conform the analytical investigation and accuracy of proposed model.
2020-01-27
Salamai, Abdullah, Hussain, Omar, Saberi, Morteza.  2019.  Decision Support System for Risk Assessment Using Fuzzy Inference in Supply Chain Big Data. 2019 International Conference on High Performance Big Data and Intelligent Systems (HPBD IS). :248–253.

Currently, organisations find it difficult to design a Decision Support System (DSS) that can predict various operational risks, such as financial and quality issues, with operational risks responsible for significant economic losses and damage to an organisation's reputation in the market. This paper proposes a new DSS for risk assessment, called the Fuzzy Inference DSS (FIDSS) mechanism, which uses fuzzy inference methods based on an organisation's big data collection. It includes the Emerging Association Patterns (EAP) technique that identifies the important features of each risk event. Then, the Mamdani fuzzy inference technique and several membership functions are evaluated using the firm's data sources. The FIDSS mechanism can enhance an organisation's decision-making processes by quantifying the severity of a risk as low, medium or high. When it automatically predicts a medium or high level, it assists organisations in taking further actions that reduce this severity level.

Akinrolabu, Olusola, New, Steve, Martin, Andrew.  2019.  Assessing the Security Risks of Multicloud SaaS Applications: A Real-World Case Study. 2019 6th IEEE International Conference on Cyber Security and Cloud Computing (CSCloud)/ 2019 5th IEEE International Conference on Edge Computing and Scalable Cloud (EdgeCom). :81–88.

Cloud computing is widely believed to be the future of computing. It has grown from being a promising idea to one of the fastest research and development paradigms of the computing industry. However, security and privacy concerns represent a significant hindrance to the widespread adoption of cloud computing services. Likewise, the attributes of the cloud such as multi-tenancy, dynamic supply chain, limited visibility of security controls and system complexity, have exacerbated the challenge of assessing cloud risks. In this paper, we conduct a real-world case study to validate the use of a supply chaininclusive risk assessment model in assessing the risks of a multicloud SaaS application. Using the components of the Cloud Supply Chain Cyber Risk Assessment (CSCCRA) model, we show how the model enables cloud service providers (CSPs) to identify critical suppliers, map their supply chain, identify weak security spots within the chain, and analyse the risk of the SaaS application, while also presenting the value of the risk in monetary terms. A key novelty of the CSCCRA model is that it caters for the complexities involved in the delivery of SaaS applications and adapts to the dynamic nature of the cloud, enabling CSPs to conduct risk assessments at a higher frequency, in response to a change in the supply chain.

2020-01-20
Ingols, Kyle, Chu, Matthew, Lippmann, Richard, Webster, Seth, Boyer, Stephen.  2009.  Modeling Modern Network Attacks and Countermeasures Using Attack Graphs. 2009 Annual Computer Security Applications Conference. :117–126.
By accurately measuring risk for enterprise networks, attack graphs allow network defenders to understand the most critical threats and select the most effective countermeasures. This paper describes substantial enhancements to the NetSPA attack graph system required to model additional present-day threats (zero-day exploits and client-side attacks) and countermeasures (intrusion prevention systems, proxy firewalls, personal firewalls, and host-based vulnerability scans). Point-to-point reachability algorithms and structures were extensively redesigned to support "reverse" reachability computations and personal firewalls. Host-based vulnerability scans are imported and analyzed. Analysis of an operational network with 84 hosts demonstrates that client-side attacks pose a serious threat. Experiments on larger simulated networks demonstrated that NetSPA's previous excellent scaling is maintained. Less than two minutes are required to completely analyze a four-enclave simulated network with more than 40,000 hosts protected by personal firewalls.
Gay, Maël, Paxian, Tobias, Upadhyaya, Devanshi, Becker, Bernd, Polian, Ilia.  2019.  Hardware-Oriented Algebraic Fault Attack Framework with Multiple Fault Injection Support. 2019 Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC). :25–32.

The evaluation of fault attacks on security-critical hardware implementations of cryptographic primitives is an important concern. In such regards, we have created a framework for automated construction of fault attacks on hardware realization of ciphers. The framework can be used to quickly evaluate any cipher implementations, including any optimisations. It takes the circuit description of the cipher and the fault model as input. The output of the framework is a set of algebraic equations, such as conjunctive normal form (CNF) clauses, which is then fed to a SAT solver. We consider both attacking an actual implementation of a cipher on an field-programmable gate array (FPGA) platform using a fault injector and the evaluation of an early design of the cipher using idealized fault models. We report the successful application of our hardware-oriented framework to a collection of ciphers, including the advanced encryption standard (AES), and the lightweight block ciphers LED and PRESENT. The corresponding results and a discussion of the impact to different fault models on our framework are shown. Moreover, we report significant improvements compared to similar frameworks, such as speedups or more advanced features. Our framework is the first algebraic fault attack (AFA) tool to evaluate the state-of-the art cipher LED-64, PRESENT and full-scale AES using only hardware-oriented structural cipher descriptions.

2020-01-02
Mar\'ın, Gonzalo, Casas, Pedro, Capdehourat, Germán.  2019.  Deep in the Dark - Deep Learning-Based Malware Traffic Detection Without Expert Knowledge. 2019 IEEE Security and Privacy Workshops (SPW). :36–42.

With the ever-growing occurrence of networking attacks, robust network security systems are essential to prevent and mitigate their harming effects. In recent years, machine learning-based systems have gain popularity for network security applications, usually considering the application of shallow models, where a set of expert handcrafted features are needed to pre-process the data before training. The main problem with this approach is that handcrafted features can fail to perform well given different kinds of scenarios and problems. Deep Learning models can solve this kind of issues using their ability to learn feature representations from input raw or basic, non-processed data. In this paper we explore the power of deep learning models on the specific problem of detection and classification of malware network traffic, using different representations for the input data. As a major advantage as compared to the state of the art, we consider raw measurements coming directly from the stream of monitored bytes as the input to the proposed models, and evaluate different raw-traffic feature representations, including packet and flow-level ones. Our results suggest that deep learning models can better capture the underlying statistics of malicious traffic as compared to classical, shallow-like models, even while operating in the dark, i.e., without any sort of expert handcrafted inputs.

2019-12-02
Yang, Shouguo, Shi, Zhiqiang, Zhang, Guodong, Li, Mingxuan, Ma, Yuan, Sun, Limin.  2019.  Understand Code Style: Efficient CNN-Based Compiler Optimization Recognition System. ICC 2019 - 2019 IEEE International Conference on Communications (ICC). :1–6.
Compiler optimization level recognition can be applied to vulnerability discovery and binary analysis. Due to the exists of many different compilation optimization options, the difference in the contents of the binary file is very complicated. There are thousands of compiler optimization algorithms and multiple different processor architectures, so it is very difficult to manually analyze binary files and recognize its compiler optimization level with rules. This paper first proposes a CNN-based compiler optimization level recognition model: BinEye. The system extracts semantic and structural differences and automatically recognize the compiler optimization levels. The model is designed to be very suitable for binary file processing and is easy to understand. We built a dataset containing 80028 binary files for the model training and testing. Our proposed model achieves an accuracy of over 97%. At the same time, BinEye is a fully CNN-based system and it has a faster forward calculation speed, at least 8 times faster than the normal RNN-based model. Through our analysis of the model output, we successfully found the difference in assembly codes caused by the different compiler optimization level. This means that the model we proposed is interpretable. Based on our model, we propose a method to analyze the code differences caused by different compiler optimization levels, which has great guiding significance for analyzing closed source compilers and binary security analysis.
2019-11-19
Ying, Huan, Zhang, Yanmiao, Han, Lifang, Cheng, Yushi, Li, Jiyuan, Ji, Xiaoyu, Xu, Wenyuan.  2019.  Detecting Buffer-Overflow Vulnerabilities in Smart Grid Devices via Automatic Static Analysis. 2019 IEEE 3rd Information Technology, Networking, Electronic and Automation Control Conference (ITNEC). :813-817.

As a modern power transmission network, smart grid connects plenty of terminal devices. However, along with the growth of devices are the security threats. Different from the previous separated environment, an adversary nowadays can destroy the power system by attacking these devices. Therefore, it's critical to ensure the security and safety of terminal devices. To achieve this goal, detecting the pre-existing vulnerabilities of the device program and enhance the terminal security, are of great importance and necessity. In this paper, we propose a novel approach that detects existing buffer-overflow vulnerabilities of terminal devices via automatic static analysis (ASA). We utilize the static analysis to extract the device program information and build corresponding program models. By further matching the generated program model with pre-defined vulnerability patterns, we achieve vulnerability detection and error reporting. The evaluation results demonstrate that our method can effectively detect buffer-overflow vulnerabilities of smart terminals with a high accuracy and a low false positive rate.

2019-11-12
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.

2019-09-04
Lawson, M., Lofstead, J..  2018.  Using a Robust Metadata Management System to Accelerate Scientific Discovery at Extreme Scales. 2018 IEEE/ACM 3rd International Workshop on Parallel Data Storage Data Intensive Scalable Computing Systems (PDSW-DISCS). :13–23.
Our previous work, which can be referred to as EMPRESS 1.0, showed that rich metadata management provides a relatively low-overhead approach to facilitating insight from scale-up scientific applications. However, this system did not provide the functionality needed for a viable production system or address whether such a system could scale. Therefore, we have extended our previous work to create EMPRESS 2.0, which incorporates the features required for a useful production system. Through a discussion of EMPRESS 2.0, this paper explores how to incorporate rich query functionality, fault tolerance, and atomic operations into a scalable, storage system independent metadata management system that is easy to use. This paper demonstrates that such a system offers significant performance advantages over HDF5, providing metadata querying that is 150X to 650X faster, and can greatly accelerate post-processing. Finally, since the current implementation of EMPRESS 2.0 relies on an RDBMS, this paper demonstrates that an RDBMS is a viable technology for managing data-oriented metadata.
2019-08-26
Zhang, Y., Ya\u gan, O..  2018.  Modeling and Analysis of Cascading Failures in Interdependent Cyber-Physical Systems. 2018 IEEE Conference on Decision and Control (CDC). :4731-4738.

Integrated cyber-physical systems (CPSs), such as the smart grid, are becoming the underpinning technology for major industries. A major concern regarding such systems are the seemingly unexpected large scale failures, which are often attributed to a small initial shock getting escalated due to intricate dependencies within and across the individual counterparts of the system. In this paper, we develop a novel interdependent system model to capture this phenomenon, also known as cascading failures. Our framework consists of two networks that have inherently different characteristics governing their intra-dependency: i) a cyber-network where a node is deemed to be functional as long as it belongs to the largest connected (i.e., giant) component; and ii) a physical network where nodes are given an initial flow and a capacity, and failure of a node results with redistribution of its flow to the remaining nodes, upon which further failures might take place due to overloading. Furthermore, it is assumed that these two networks are inter-dependent. For simplicity, we consider a one-to-one interdependency model where every node in the cyber-network is dependent upon and supports a single node in the physical network, and vice versa. We provide a thorough analysis of the dynamics of cascading failures in this interdependent system initiated with a random attack. The system robustness is quantified as the surviving fraction of nodes at the end of cascading failures, and is derived in terms of all network parameters involved. Analytic results are supported through an extensive numerical study. Among other things, these results demonstrate the ability of our model to capture the unexpected nature of large-scale failures, and provide insights on improving system robustness.

2019-06-28
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.