Visible to the public Biblio

Found 784 results

Filters: First Letter Of Last Name is K  [Clear All Filters]
A B C D E F G H I J [K] L M N O P Q R S T U V W X Y Z   [Show ALL]
Kamalraj, R., Madhan, E.S., Ghamya, K., Bhargavi, V..  2020.  Enhance Safety and Security System for Children in School Campus by using Wearable Sensors. 2020 Fourth International Conference on Computing Methodologies and Communication (ICCMC). :986—990.
Child security in the school campus is most important in building a good society. In and around the world the children are abused and killed also in sometimes by the people those who are not in good attitude in the school campus. To track and resolve such issues an enhanced security feature system is required. Hence in this paper an enhanced version of security system for children is proposed by using `Wearable Sensors'. In this proposed method two wearable sensors nodes such as `Staff Node' and `Student Node' are paired by using `Bluetooth' communication technology and Smart Watch technology is also used to communicate the Security Center or Processing Node for tracking them about their location and whether the two nodes are moved away from the classroom. If the child node is not moving for a long period then it may be notified by the center and they will inform the security officers near to the place. This proposed method may satisfy the need of school management about the staff movements with students and the behavior of students to avoid unexpected issues.
Kamdem, G., Kamhoua, C., Lu, Y., Shetty, S., Njilla, L..  2017.  A Markov Game Theoritic Approach for Power Grid Security. 2017 IEEE 37th International Conference on Distributed Computing Systems Workshops (ICDCSW). :139–144.

The extensive use of information and communication technologies in power grid systems make them vulnerable to cyber-attacks. One class of cyber-attack is advanced persistent threats where highly skilled attackers can steal user authentication information's and then move laterally in the network, from host to host in a hidden manner, until they reach an attractive target. Once the presence of the attacker has been detected in the network, appropriate actions should be taken quickly to prevent the attacker going deeper. This paper presents a game theoretic approach to optimize the defense against an invader attempting to use a set of known vulnerabilities to reach critical nodes in the network. First, the network is modeled as a vulnerability multi-graph where the nodes represent physical hosts and edges the vulnerabilities that the attacker can exploit to move laterally from one host to another. Secondly, a two-player zero-sum Markov game is built where the states of the game represent the nodes of the vulnerability multi-graph graph and transitions correspond to the edge vulnerabilities that the attacker can exploit. The solution of the game gives the optimal strategy to disconnect vulnerable services and thus slow down the attack.

Kamel, M. B. M., Alameri, I., Onaizah, A. N..  2017.  STAODV: A secure and trust based approach to mitigate blackhole attack on AODV based MANET. 2017 IEEE 2nd Advanced Information Technology, Electronic and Automation Control Conference (IAEAC). :1278–1282.

Mobile ad hoc networks (MANET) is a type of networks that consists of autonomous nodes connecting directly without a top-down network architecture or central controller. Absence of base stations in MANET force the nodes to rely on their adjacent nodes in transmitting messages. The dynamic nature of MANET makes the relationship between nodes untrusted due to mobility of nodes. A malicious node may start denial of service attack at network layer to discard the packets instead of forwarding them to destination which is known as black hole attack. In this paper a secure and trust based approach based on ad hoc on demand distance vector (STAODV) has been proposed to improve the security of AODV routing protocol. The approach isolates the malicious nodes that try to attack the network depending on their previous information. A trust level is attached to each participating node to detect the level of trust of that node. Each incoming packet will be examined to prevent the black hole attack.

Kamhoua, C. A..  2018.  Game theoretic modeling of cyber deception in the Internet of Battlefield Things. 2018 56th Annual Allerton Conference on Communication, Control, and Computing (Allerton). :862—862.

Internet of Battlefield Things (IoBT) devices such as actuators, sensors, wearable devises, robots, drones, and autonomous vehicles, facilitate the Intelligence, Surveillance and Reconnaissance (ISR) to Command and Control and battlefield services. IoBT devices have the ability to collect operational field data, to compute on the data, and to upload its information to the network. Securing the IoBT presents additional challenges compared with traditional information technology (IT) systems. First, IoBT devices are mass produced rapidly to be low-cost commodity items without security protection in their original design. Second, IoBT devices are highly dynamic, mobile, and heterogeneous without common standards. Third, it is imperative to understand the natural world, the physical process(es) under IoBT control, and how these real-world processes can be compromised before recommending any relevant security counter measure. Moreover, unprotected IoBT devices can be used as “stepping stones” by attackers to launch more sophisticated attacks such as advanced persistent threats (APTs). As a result of these challenges, IoBT systems are the frequent targets of sophisticated cyber attack that aim to disrupt mission effectiveness.

Kamilin, M. H. B., Yamaguchi, S..  2020.  White-Hat Worm Launcher Based on Deep Learning in Botnet Defense System. 2020 IEEE International Conference on Consumer Electronics - Asia (ICCE-Asia). :1—2.

This paper proposes a deep learning-based white-hat worm launcher in Botnet Defense System (BDS). BDS uses white-hat botnets to defend an IoT system against malicious botnets. White-hat worm launcher literally launches white-hat worms to create white-hat botnets according to the strategy decided by BDS. The proposed launcher learns with deep learning where is the white-hat worms' right place to successfully drive out malicious botnets. Given a system situation invaded by malicious botnets, it predicts a worms' placement by the learning result and launches them. We confirmed the effect of the proposed launcher through simulating evaluation.

Kaminski, Ted, Van Wyk, Eric.  2017.  Ensuring Non-Interference of Composable Language Extensions. Proceedings of the 10th ACM SIGPLAN International Conference on Software Language Engineering. :163–174.

Extensible language frameworks aim to allow independently-developed language extensions to be easily added to a host programming language. It should not require being a compiler expert, and the resulting compiler should "just work" as expected. Previous work has shown how specifications for parsing (based on context free grammars) and for semantic analysis (based on attribute grammars) can be automatically and reliably composed, ensuring that the resulting compiler does not terminate abnormally. However, this work does not ensure that a property proven to hold for a language (or extended language) still holds when another extension is added, a problem we call interference. We present a solution to this problem using of a logical notion of coherence. We show that a useful class of language extensions, implemented as attribute grammars, preserve all coherent properties. If we also restrict extensions to only making use of coherent properties in establishing their correctness, then the correctness properties of each extension will hold when composed with other extensions. As a result, there can be no interference: each extension behaves as specified.

Kammuller, F..  2014.  Verification of DNSsec Delegation Signatures. Telecommunications (ICT), 2014 21st International Conference on. :298-392.

In this paper, we present a formal model for the verification of the DNSsec Protocol in the interactive theorem prover Isabelle/HOL. Relying on the inductive approach to security protocol verification, this formal analysis provides a more expressive representation than the widely accepted model checking analysis. Our mechanized model allows to represent the protocol, all its possible traces and the attacker and his knowledge. The fine grained model allows to show origin authentication, and replay attack prevention. Most prominently, we succeed in expressing Delegation Signatures and proving their authenticity formally.

Kamoona, M., El-Sharkawy, M..  2016.  FlexiWi-Fi Security Manager Using Freescale Embedded System. 2015 2nd International Conference on Information Science and Security (ICISS). :1–4.

Among the current Wi-Fi two security models (Enterprise and Personal), while the Enterprise model (802.1X) offers an effective framework for authenticating and controlling the user traffic to a protected network, the Personal model (802.11) offers the cheapest and the easiest to setup solution. However, the drawback of the personal model implementation is that all access points and client radio NIC on the wireless LAN should use the same encryption key. A major underlying problem of the 802.11 standard is that the pre-shared keys are cumbersome to change. So if those keys are not updated frequently, unauthorized users with some resources and within a short timeframe can crack the key and breach the network security. The purpose of this paper is to propose and implement an effective method for the system administrator to manage the users connected to a router, update the keys and further distribute them for the trusted clients using the Freescale embedded system, Infrared and Bluetooth modules.

Kampanakis, P., Perros, H., Beyene, T..  2014.  SDN-based solutions for Moving Target Defense network protection. A World of Wireless, Mobile and Multimedia Networks (WoWMoM), 2014 IEEE 15th International Symposium on. :1-6.

Software-Defined Networking (SDN) allows network capabilities and services to be managed through a central control point. Moving Target Defense (MTD) on the other hand, introduces a constantly adapting environment in order to delay or prevent attacks on a system. MTD is a use case where SDN can be leveraged in order to provide attack surface obfuscation. In this paper, we investigate how SDN can be used in some network-based MTD techniques. We first describe the advantages and disadvantages of these techniques, the potential countermeasures attackers could take to circumvent them, and the overhead of implementing MTD using SDN. Subsequently, we study the performance of the SDN-based MTD methods using Cisco's One Platform Kit and we show that they significantly increase the attacker's overheads.

Kan Yang, Xiaohua Jia, Kui Ren, Ruitao Xie, Liusheng Huang.  2014.  Enabling efficient access control with dynamic policy updating for big data in the cloud. INFOCOM, 2014 Proceedings IEEE. :2013-2021.

Due to the high volume and velocity of big data, it is an effective option to store big data in the cloud, because the cloud has capabilities of storing big data and processing high volume of user access requests. Attribute-Based Encryption (ABE) is a promising technique to ensure the end-to-end security of big data in the cloud. However, the policy updating has always been a challenging issue when ABE is used to construct access control schemes. A trivial implementation is to let data owners retrieve the data and re-encrypt it under the new access policy, and then send it back to the cloud. This method incurs a high communication overhead and heavy computation burden on data owners. In this paper, we propose a novel scheme that enabling efficient access control with dynamic policy updating for big data in the cloud. We focus on developing an outsourced policy updating method for ABE systems. Our method can avoid the transmission of encrypted data and minimize the computation work of data owners, by making use of the previously encrypted data with old access policies. Moreover, we also design policy updating algorithms for different types of access policies. The analysis show that our scheme is correct, complete, secure and efficient.

Kan-Siew-Leong, Chze, P. L. R., Wee, A. K., Sim, E., May, K. E..  2017.  A multi-factors security key generation mechanism for IoT. 2017 Ninth International Conference on Ubiquitous and Future Networks (ICUFN). :1019–1021.

This paper introduces a multi-factors security key generation mechanism for self-organising Internet of Things (IoT) network and nodes. The mechanism enables users to generate unique set of security keys to enhance IoT security while meeting various business needs. The multi-factor security keys presents an additional security layer to existing security standards and practices currently being adopted by the IoT community. The proposed security key generation mechanism enables user to define and choose any physical and logical parameters he/she prefers, in generating a set of security keys to be encrypted and distributed to registered IoT nodes. IoT applications and services will only be activated after verifying that all security keys are present. Multiple levels of authorisation for different user groups can be easily created through the mix and match of the generated multi-factors security keys. A use case, covering indoor and outdoor field tests was conducted. The results of the tests showed that the mechanism is easily adaptable to meet diverse multivendor IoT devices and is scalable for various applications.

Kandah, Farah, Cancelleri, Joseph, Reising, Donald, Altarawneh, Amani, Skjellum, Anthony.  2019.  A Hardware-Software Codesign Approach to Identity, Trust, and Resilience for IoT/CPS at Scale. 2019 International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData). :1125–1134.
Advancement in communication technologies and the Internet of Things (IoT) is driving adoption in smart cities that aims to increase operational efficiency and improve the quality of services and citizen welfare, among other potential benefits. The privacy, reliability, and integrity of communications must be ensured so that actions can be appropriate, safe, accurate, and implemented promptly after receiving actionable information. In this work, we present a multi-tier methodology consisting of an authentication and trust-building/distribution framework designed to ensure the safety and validity of the information exchanged in the system. Blockchain protocols and Radio Frequency-Distinct Native Attributes (RF-DNA) combine to provide a hardware-software codesigned system for enhanced device identity and overall system trustworthiness. Our threat model accounts for counterfeiting, breakout fraud, and bad mouthing of one entity by others. Entity trust (e.g., IoT devices) depends on quality and level of participation, quality of messages, lifetime of a given entity in the system, and the number of known "bad" (non-consensus) messages sent by that entity. Based on this approach to trust, we are able to adjust trust upward and downward as a function of real-time and past behavior, providing other participants with a trust value upon which to judge information from and interactions with the given entity. This approach thereby reduces the potential for manipulation of an IoT system by a bad or byzantine actor.
Kandoussi, El Mehdi, El Mir, Iman, Hanini, Mohamed, Haqiq, Abdelkrim.  2019.  Modeling Virtual Machine Migration as a Security Mechanism by using Continuous-Time Markov Chain Model. 2019 4th World Conference on Complex Systems (WCCS). :1–6.

In Cloud Computing Environment, using only static security measures didn't mitigate the attack considerably. Hence, deployment of sophisticated methods by the attackers to understand the network topology of complex network makes the task easier. For this reason, the use of dynamic security measure as virtual machine (VM) migration increases uncertainty to locate a virtual machine in a dynamic attack surface. Although this, not all VM's migration enhances security. Indeed, the destination server to host the VM should be selected precisely in order to avoid externality and attack at the same time. In this paper, we model migration in cloud environment by using continuous Markov Chain. Then, we analyze the probability of a VM to be compromised based on the destination server parameters. Finally, we provide some numerical results to show the effectiveness of our approach in term of avoiding intrusion.

Kane, Andrew, Tompa, Frank Wm..  2017.  Small-Term Distribution for Disk-Based Search. Proceedings of the 2017 ACM Symposium on Document Engineering. :49–58.

A disk-based search system distributes a large index across multiple disks on one or more machines, where documents are typically assigned to disks at random in order to achieve load balancing. However, random distribution degrades clustering, which is required for efficient index compression. Using the GOV2 dataset, we demonstrate the effect of various ordering techniques on index compression, and then quantify the effect of various document distribution approaches on compression and load balancing. We explore runtime performance by simulating a disk-based search system for a scaled-out 10xGOV2 index over ten disks using two standard approaches, document and term distribution, as well as a hybrid approach: small-term distribution. We find that small-term distribution has the best performance, especially in the presence of list caching, and argue that this rarely discussed distribution approach can improve disk-based search performance for many real-world installations.

Kanellopoulos, Aris, Vamvoudakis, Kyriakos G., Gupta, Vijay.  2019.  Decentralized Verification for Dissipativity of Cascade Interconnected Systems. 2019 IEEE 58th Conference on Decision and Control (CDC). :3629—3634.

In this paper, we consider the problem of decentralized verification for large-scale cascade interconnections of linear subsystems such that dissipativity properties of the overall system are guaranteed with minimum knowledge of the dynamics. In order to achieve compositionality, we distribute the verification process among the individual subsystems, which utilize limited information received locally from their immediate neighbors. Furthermore, to obviate the need for full knowledge of the subsystem parameters, each decentralized verification rule employs a model-free learning structure; a reinforcement learning algorithm that allows for online evaluation of the appropriate storage function that can be used to verify dissipativity of the system up to that point. Finally, we show how the interconnection can be extended by adding learning-enabled subsystems while ensuring dissipativity.

Kanemura, Kota, Toyoda, Kentaroh, Ohtsuki, Tomoaki.  2019.  Identification of Darknet Markets’ Bitcoin Addresses by Voting Per-address Classification Results. 2019 IEEE International Conference on Blockchain and Cryptocurrency (ICBC). :154—158.
Bitcoin is a decentralized digital currency whose transactions are recorded in a common ledger, so called blockchain. Due to the anonymity and lack of law enforcement, Bitcoin has been misused in darknet markets which deal with illegal products, such as drugs and weapons. Therefore from the security forensics aspect, it is demanded to establish an approach to identify newly emerged darknet markets' transactions and addresses. In this paper, we thoroughly analyze Bitcoin transactions and addresses related to darknet markets and propose a novel identification method of darknet markets' addresses. To improve the identification performance, we propose a voting based method which decides the labels of multiple addresses controlled by the same user based on the number of the majority label. Through the computer simulation with more than 200K Bitcoin addresses, it was shown that our voting based method outperforms the nonvoting based one in terms of precision, recal, and F1 score. We also found that DNM's addresses pay higher fees than others, which significantly improves the classification.
Kaneriya, J., Patel, H..  2020.  A Comparative Survey on Blockchain Based Self Sovereign Identity System. 2020 3rd International Conference on Intelligent Sustainable Systems (ICISS). :1150—1155.

The Internet has changed business, education, healthcare, banking etc. and it is the main part of technological evolution. Internet provides us a connecting world to perform our day to day life activities easily. Internet is designed in such a way that it can uniquely identify machine, not a person, on the network hence there is need to design a system that can perform entity identification on the Internet. Currently on Internet, service providers provide identity of a user with user name and password and store this information on a centralized server. These servers become honey pot for hackers to steal user’s personal identity information and service provider can utilize user identity information using data mining, artificial intelligence for economic benefits. Aim of Self sovereign identity system is to provide decentralized, user centric identity system which is controlled by identity owner that can be developed along with distributed ledger technology i.e. blockchain. In this paper, we intend to make an exhaustive study on different blockchain based self sovereign identity implementations (such as Sovrin, Uport, EverID, LifeID, Sora, SelfKey) along with its architectural components and discuss about use case of self sovereign identity.

Kanewala, T.A., Marru, S., Basney, J., Pierce, M..  2014.  A Credential Store for Multi-tenant Science Gateways. Cluster, Cloud and Grid Computing (CCGrid), 2014 14th IEEE/ACM International Symposium on. :445-454.

Science Gateways bridge multiple computational grids and clouds, acting as overlay cyber infrastructure. Gateways have three logical tiers: a user interfacing tier, a resource tier and a bridging middleware tier. Different groups may operate these tiers. This introduces three security challenges. First, the gateway middleware must manage multiple types of credentials associated with different resource providers. Second, the separation of the user interface and middleware layers means that security credentials must be securely delegated from the user interface to the middleware. Third, the same middleware may serve multiple gateways, so the middleware must correctly isolate user credentials associated with different gateways. We examine each of these three scenarios, concentrating on the requirements and implementation of the middleware layer. We propose and investigate the use of a Credential Store to solve the three security challenges.

Kanewala, Thejaka Amila, Zalewski, Marcin, Lumsdaine, Andrew.  2018.  Distributed, Shared-Memory Parallel Triangle Counting. Proceedings of the Platform for Advanced Scientific Computing Conference. :5:1–5:12.
Triangles are the most basic non-trivial subgraphs. Triangle counting is used in a number of different applications, including social network mining, cyber security, and spam detection. In general, triangle counting algorithms are readily parallelizable, but when implemented in distributed, shared-memory, their performance is poor due to high communication, imbalance of work, and the difficulty of exploiting locality available in shared memory. In this paper, we discuss four different (but related) triangle counting algorithms and how their performance can be improved in distributed, shared-memory by reducing in-node load imbalance, improving cache utilization, minimizing network overhead, and minimizing algorithmic work. We generalize the four different triangle counting algorithms into a common framework and show that for all four algorithms the in-node load imbalance can be minimized while utilizing caches by partitioning work into blocks of vertices, the network overhead can be minimized by aggregation of blocks of work, and algorithm work can be reduced by partitioning vertex neighbors by degree. We experimentally evaluate the weak and the strong scaling performance of the proposed algorithms with two types of synthetic graph inputs and three real-world graph inputs. We also compare the performance of our implementations with the distributed, shared-memory triangle counting algorithms available in PowerGraph-GraphLab and show that our proposed algorithms outperform those algorithms, both in terms of space and time.
Kang, Anqi.  2018.  Collaborative Filtering Algorithm Based on Trust and Information Entropy. 2018 International Conference on Intelligent Informatics and Biomedical Sciences (ICIIBMS). 3:262—266.

In order to improve the accuracy of similarity, an improved collaborative filtering algorithm based on trust and information entropy is proposed in this paper. Firstly, the direct trust between the users is determined by the user's rating to explore the potential trust relationship of the users. The time decay function is introduced to realize the dynamic portrayal of the user's interest decays over time. Secondly, the direct trust and the indirect trust are combined to obtain the overall trust which is weighted with the Pearson similarity to obtain the trust similarity. Then, the information entropy theory is introduced to calculate the similarity based on weighted information entropy. At last, the trust similarity and the similarity based on weighted information entropy are weighted to obtain the similarity combing trust and information entropy which is used to predicted the rating of the target user and create the recommendation. The simulation shows that the improved algorithm has a higher accuracy of recommendation and can provide more accurate and reliable recommendation service.

Kang, Chanhyun, Park, Noseong, Prakash, B. Aditya, Serra, Edoardo, Subrahmanian, V. S..  2016.  Ensemble Models for Data-driven Prediction of Malware Infections. Proceedings of the Ninth ACM International Conference on Web Search and Data Mining. :583–592.

Given a history of detected malware attacks, can we predict the number of malware infections in a country? Can we do this for different malware and countries? This is an important question which has numerous implications for cyber security, right from designing better anti-virus software, to designing and implementing targeted patches to more accurately measuring the economic impact of breaches. This problem is compounded by the fact that, as externals, we can only detect a fraction of actual malware infections. In this paper we address this problem using data from Symantec covering more than 1.4 million hosts and 50 malware spread across 2 years and multiple countries. We first carefully design domain-based features from both malware and machine-hosts perspectives. Secondly, inspired by epidemiological and information diffusion models, we design a novel temporal non-linear model for malware spread and detection. Finally we present ESM, an ensemble-based approach which combines both these methods to construct a more accurate algorithm. Using extensive experiments spanning multiple malware and countries, we show that ESM can effectively predict malware infection ratios over time (both the actual number and trend) upto 4 times better compared to several baselines on various metrics. Furthermore, ESM's performance is stable and robust even when the number of detected infections is low.

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.
Kang, E. Y., Mu, D., Huang, L., Lan, Q..  2017.  Verification and Validation of a Cyber-Physical System in the Automotive Domain. 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :326–333.
Software development for Cyber-Physical Systems (CPS), e.g., autonomous vehicles, requires both functional and non-functional quality assurance to guarantee that the CPS operates safely and effectively. EAST-ADL is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time (ERT) behaviors modeled in EAST-ADL/Stateflow into UPPAAL models amenable to formal verification. Previous work is extended in this paper by including support for Simulink and an integration of Simulink/Stateflow (S/S) within the same too lchain. S/S models are transformed, based on the extended ERT constraints with probability parameters, into verifiable UPPAAL-SMC models and integrate the translation with formal statistical analysis techniques: Probabilistic extension of EAST-ADL constraints is defined as a semantics denotation. A set of mapping rules is proposed to facilitate the guarantee of translation. Formal analysis on both functional- and non-functional properties is performed using Simulink Design Verifier and UPPAAL-SMC. Our approach is demonstrated on the autonomous traffic sign recognition vehicle case study.
Kang, Eunsuk, Adepu, Sridhar, Jackson, Daniel, Mathur, Aditya P..  2016.  Model-based Security Analysis of a Water Treatment System. Proceedings of the 2Nd International Workshop on Software Engineering for Smart Cyber-Physical Systems. :22–28.

An approach to analyzing the security of a cyber-physical system (CPS) is proposed, where the behavior of a physical plant and its controller are captured in approximate models, and their interaction is rigorously checked to discover potential attacks that involve a varying number of compromised sensors and actuators. As a preliminary study, this approach has been applied to a fully functional water treatment testbed constructed at the Singapore University of Technology and Design. The analysis revealed previously unknown attacks that were confirmed to pose serious threats to the safety of the testbed, and suggests a number of research challenges and opportunities for applying a similar type of formal analysis to cyber-physical security.

Kang, Eunsuk, Milicevic, Aleksandar, Jackson, Daniel.  2016.  Multi-representational Security Analysis. Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. :181–192.

Security attacks often exploit flaws that are not anticipated in an abstract design, but are introduced inadvertently when high-level interactions in the design are mapped to low-level behaviors in the supporting platform. This paper proposes a multi-representational approach to security analysis, where models capturing distinct (but possibly overlapping) views of a system are automatically composed in order to enable an end-to-end analysis. This approach allows the designer to incrementally explore the impact of design decisions on security, and discover attacks that span multiple layers of the system. This paper describes Poirot, a prototype implementation of the approach, and reports on our experience on applying Poirot to detect previously unknown security flaws in publicly deployed systems.