Visible to the public Biblio

Found 12044 results

Filters: Keyword is Resiliency  [Clear All Filters]
2017-10-27
Pedraza-García, Gilberto, Noël, René, Matalonga, Santiago, Astudillo, Hernán, Fernandez, Eduardo B..  2016.  Mitigating Security Threats Using Tactics and Patterns: A Controlled Experiment. Proccedings of the 10th European Conference on Software Architecture Workshops. :37:1–37:7.
Security Patterns and Architectural Tactics are two well-known techniques for designing secure software systems. There is little or no empirical evidence on their relative effectiveness for security threats mitigation. This study presents MUA (Misuse activities + Patterns), an extension of misuse activities that incorporates patterns, and reports on a controlled comparison of this method that incorporate these techniques for threat mitigation with regard to MAST (Methodology for Applying Security Tactics) which already incorporates tactics. A simple Tsunami Alert System design was analyzed and modified by 40 undergraduate students, and significant difference was found for security threats mitigation (averaging 3.0 for Patterns versus 1.9 for Tactics, in a 1-to-5 scale). This result is contrary to previous results with professional subjects, leading us to believe that novices benefit more of detailed advice than of high-level concepts.
2017-10-19
Ko, Wilson K.H., Wu, Yan, Tee, Keng Peng.  2016.  LAP: A Human-in-the-loop Adaptation Approach for Industrial Robots. Proceedings of the Fourth International Conference on Human Agent Interaction. :313–319.

In the last few years, a shift from mass production to mass customisation is observed in the industry. Easily reprogrammable robots that can perform a wide variety of tasks are desired to keep up with the trend of mass customisation while saving costs and development time. Learning by Demonstration (LfD) is an easy way to program the robots in an intuitive manner and provides a solution to this problem. In this work, we discuss and evaluate LAP, a three-stage LfD method that conforms to the criteria for the high-mix-low-volume (HMLV) industrial settings. The algorithm learns a trajectory in the task space after which small segments can be adapted on-the-fly by using a human-in-the-loop approach. The human operator acts as a high-level adaptation, correction and evaluation mechanism to guide the robot. This way, no sensors or complex feedback algorithms are needed to improve robot behaviour, so errors and inaccuracies induced by these subsystems are avoided. After the system performs at a satisfactory level after the adaptation, the operator will be removed from the loop. The robot will then proceed in a feed-forward fashion to optimise for speed. We demonstrate this method by simulating an industrial painting application. A KUKA LBR iiwa is taught how to draw an eight figure which is reshaped by the operator during adaptation.

Wu, Wenfei, Zhang, Ying, Banerjee, Sujata.  2016.  Automatic Synthesis of NF Models by Program Analysis. Proceedings of the 15th ACM Workshop on Hot Topics in Networks. :29–35.

Network functions (NFs), like firewall, NAT, IDS, have been widely deployed in today’s modern networks. However, currently there is no standard specification or modeling language that can accurately describe the complexity and diversity of different NFs. Recently there have been research efforts to propose NF models. However, they are often generated manually and thus error-prone. This paper proposes a method to automatically synthesize NF models via program analysis. We develop a tool called NFactor, which conducts code refactoring and program slicing on NF source code, in order to generate its forwarding model. We demonstrate its usefulness on two NFs and evaluate its correctness. A few applications of NFactor are described, including network verification.

Zhang, Peng, Li, Hao, Hu, Chengchen, Hu, Liujia, Xiong, Lei, Wang, Ruilong, Zhang, Yuemei.  2016.  Mind the Gap: Monitoring the Control-Data Plane Consistency in Software Defined Networks. Proceedings of the 12th International on Conference on Emerging Networking EXperiments and Technologies. :19–33.

How to debug large networks is always a challenging task. Software Defined Network (SDN) offers a centralized con- trol platform where operators can statically verify network policies, instead of checking configuration files device-by-device. While such a static verification is useful, it is still not enough: due to data plane faults, packets may not be forwarded according to control plane policies, resulting in network faults at runtime. To address this issue, we present VeriDP, a tool that can continuously monitor what we call control-data plane consistency, defined as the consistency between control plane policies and data plane forwarding behaviors. We prototype VeriDP with small modifications of both hardware and software SDN switches, and show that it can achieve a verification speed of 3 μs per packet, with a false negative rate as low as 0.1%, for the Stanford backbone and Internet2 topologies. In addition, when verification fails, VeriDP can localize faulty switches with a probability as high as 96% for fat tree topologies.

Nikravesh, Ashkan, Hong, David Ke, Chen, Qi Alfred, Madhyastha, Harsha V., Mao, Z. Morley.  2016.  QoE Inference Without Application Control. Proceedings of the 2016 Workshop on QoE-based Analysis and Management of Data Communication Networks. :19–24.
Network quality-of-service (QoS) does not always directly translate to users' quality-of-experience (QoE), e.g., changes in a video streaming app's frame rate in reaction to changes in packet loss rate depend on various factors such as the adaptation strategy used by the app and the app's use of forward error correction (FEC) codes. Therefore, knowledge of user QoE is desirable in several scenarios that have traditionally operated on QoS information. Examples include traffic management by ISPs and resource allocation by the operating system (OS). However, today, entities such as ISPs and OSes that implement these optimizations typically do not have a convenient way of obtaining input from applications on user QoE. To address this problem, we propose offline generation of per-application models mapping application-independent QoS metrics to corresponding application-specific QoE metrics, thereby enabling entities (such as ISPs and OSes) that can observe a user's network traffic to infer the user's QoE, in the absence of direct input. In this paper, we describe how such models can be generated and present our results from two popular video applications with significantly different QoE metrics. We also showcase the use of these models for ISPs to perform QoE-aware traffic management and for the OS to offer an efficient QoE diagnosis service.
Bianco, Federica B., Koonin, Steven E., Mydlarz, Charlie, Sharma, Mohit S..  2016.  Hypertemporal Imaging of NYC Grid Dynamics: Short Paper. Proceedings of the 3rd ACM International Conference on Systems for Energy-Efficient Built Environments. :61–64.
Hypertemporal visible imaging of an urban lightscape can reveal the phase of the electrical grid granular to individual housing units. In contrast to in-situ monitoring or metering, this method offers broad, persistent, real-time, and non-permissive coverage through a single camera sited at an urban vantage point. Rapid changes in the phase of individual housing units signal changes in load (e.g., appliances turning on and off), while slower building- or neighborhood-level changes can indicate the health of distribution transformers. We demonstrate the concept by observing the 120 Hz flicker of lights across a NYC skyline. A liquid crystal shutter driven at 119.75 Hz down-converts the flicker to 0.25 Hz, which is imaged at a 4 Hz cadence by an inexpensive CCD camera; the grid phase of each source is determined by analysis of its sinusoidal light curve over an imaging "burst" of some 25 seconds. Analysis of bursts taken at \textbackslashtextasciitilde 15 minute cadence over several hours demonstrates both the stability and variation of phases of halogen, incandescent, and some fluorescent lights. Correlation of such results with ground-truth data will validate a method that could be applied to better monitor electricity consumption and distribution in both developed and developing cities.
Cheng, Lin, Tsai, Hsin-Mu, Viriyasitavat, Wantanee, Boban, Mate.  2016.  Comparison of Radio Frequency and Visible Light Propagation Channel for Vehicular Communications. Proceedings of the First ACM International Workshop on Smart, Autonomous, and Connected Vehicular Systems and Services. :66–67.
While both radio and visible light waves can serve as the transmission medium, the propagation channel plays a key role in the highly dynamic vehicular communication environment. We discuss salient properties of radio and visible light channels, including radiation pattern and path loss modeling. By comparing their similarities and highlighting the differences, we illustrate the unique capabilities and limitations of these two technologies with respect to the requirements of Cooperative Intelligent Transportation System applications.
Duque, Alexis, Stanica, Razvan, Rivano, Herve, Desportes, Adrien.  2016.  Unleashing the Power of LED-to-camera Communications for IoT Devices. Proceedings of the 3rd Workshop on Visible Light Communication Systems.
Tian, Zhao, Wright, Kevin, Zhou, Xia.  2016.  The darkLight Rises: Visible Light Communication in the Dark. Proceedings of the 22Nd Annual International Conference on Mobile Computing and Networking. :2–15.

Visible Light Communication (VLC) emerges as a new wireless communication technology with appealing benefits not present in radio communication. However, current VLC designs commonly require LED lights to emit shining light beams, which greatly limits the applicable scenarios of VLC (e.g., in a sunny day when indoor lighting is not needed). It also entails high energy overhead and unpleasant visual experiences for mobile devices to transmit data using VLC. We design and develop DarkLight, a new VLC primitive that allows light-based communication to be sustained even when LEDs emit extremely-low luminance. The key idea is to encode data into ultra-short, imperceptible light pulses. We tackle challenges in circuit designs, data encoding/decoding schemes, and DarkLight networking, to efficiently generate and reliably detect ultra-short light pulses using off-the-shelf, low-cost LEDs and photodiodes. Our DarkLight prototype supports 1.3-m distance with 1.6-Kbps data rate. By loosening up VLC's reliance on visible light beams, DarkLight presents an unconventional direction of VLC design and fundamentally broadens VLC's application scenarios.

Schmid, Stefan, Arquint, Linard, Gross, Thomas R..  2016.  Using Smartphones As Continuous Receivers in a Visible Light Communication System. Proceedings of the 3rd Workshop on Visible Light Communication Systems. :61–66.
Visible Light Communication (VLC) allows to reuse a lighting infrastructure for communication while its main purpose of illumination can be carried out at the same time. Light sources based on Light Emitting Diodes (LEDs) are attractive as they are inexpensive, ubiquitous, and allow rapid modulation. This paper describes how to integrate smartphones into such a communication system that supports networking for a wide range of devices, such as toys with single LEDs as transmitter and receivers as well as interconnected LED light bulbs. The main challenge is how to employ the smartphone without any (hardware) modification as a receiver, using the integrated camera as a (slow) light sampling device. This paper presents a simple software-based solution, exploiting the rolling shutter effect and slow motion video capturing capabilities of latest smartphones to enable continuous reception and real-time integration into an existing VLC system. Evaluation results demonstrate a working prototype and report communication distances up to 3m and a maximum data throughput of more than 1200b/s, improving upon previous work.
Shu, Xiao, Wu, Xiaolin.  2016.  Frame Untangling for Unobtrusive Display-Camera Visible Light Communication. Proceedings of the 2016 ACM on Multimedia Conference. :650–654.
Pairing displays and cameras can open up convenient and "free" visible light communication channels. But in realistic settings, the synchronization between displays (transmitters) and cameras (receivers) can be far more involved than assumed in the literature. This study aims to analyze and model the temporal behaviors of displays and cameras to make the visible light communication channel between the two more robust, while maintaining perceptual transparency of the transmitted data.
Meraoumia, Abdallah, Laimeche, Lakhdar, Bendjenna, Hakim, Chitroub, Salim.  2016.  Do We Have to Trust the Deep Learning Methods for Palmprints Identification? Proceedings of the Mediterranean Conference on Pattern Recognition and Artificial Intelligence. :85–91.
A biometric technology is an emerging field of information technology which can be used to identifying identity of unknown individual based on some characteristics derived from specific physiological and/or behavioral characteristics that the individual possesses. Thus, among several biometric characteristics, which can be derived from the hand, palmprint has been effectively used to improve identification for last years. So far, majority of research works on this biometric trait are fundamentally based on a gray-scale image which acquired using a visible light. Recently, multispectral imaging technology has been used to make the biometric system more efficient. In this work, in order to increase the discriminating ability and the classification system accuracy, we propose a multimodal system which each spectral band of palmprint operates separately and their results are fused at matching score level. In our study, each spectral band is represented by features extracted by PCANet deep learning technique. The proposed scheme is validated using the available CASIA multispectral palmprint database of 100 users. The obtained results showed that the proposed method is very efficient, which can be improved the accuracy rate.
Jardine, William, Frey, Sylvain, Green, Benjamin, Rashid, Awais.  2016.  SENAMI: Selective Non-Invasive Active Monitoring for ICS Intrusion Detection. Proceedings of the 2Nd ACM Workshop on Cyber-Physical Systems Security and Privacy. :23–34.
Current intrusion detection systems (IDS) for industrial control systems (ICS) mostly involve the retrofitting of conventional network IDSs, such as SNORT. Such an approach is prone to missing highly targeted and specific attacks against ICS. Where ICS-specific approaches exist, they often rely on passive network monitoring techniques, offering a low cost solution, and avoiding any computational overhead arising from actively polling ICS devices. However, the use of passive approaches alone could fail in the detection of attacks that alter the behaviour of ICS devices (as was the case in Stuxnet). Where active solutions exist, they can be resource-intensive, posing the risk of overloading legacy devices which are commonplace in ICSs. In this paper we aim to overcome these challenges through the combination of a passive network monitoring approach, and selective active monitoring based on attack vectors specific to an ICS context. We present the implementation of our IDS, SENAMI, for use with Siemens S7 devices. We evaluate the effectiveness of SENAMI in a comprehensive testbed environment, demonstrating validity of the proposed approach through the detection of purely passive attacks at a rate of 99%, and active value tampering attacks at a rate of 81-93%. Crucially, we reach recall values greater than 0.96, indicating few attack scenarios generating false negatives.
Udd, Robert, Asplund, Mikael, Nadjm-Tehrani, Simin, Kazemtabrizi, Mehrdad, Ekstedt, Mathias.  2016.  Exploiting Bro for Intrusion Detection in a SCADA System. Proceedings of the 2Nd ACM International Workshop on Cyber-Physical System Security. :44–51.
Supervisory control and data acquisition (SCADA) systems that run our critical infrastructure are increasingly run with Internet-based protocols and devices for remote monitoring. The embedded nature of the components involved, and the legacy aspects makes adding new security mechanisms in an efficient manner far from trivial. In this paper we study an anomaly detection based approach that enables detecting zero-day malicious threats and benign malconfigurations and mishaps. The approach builds on an existing platform (Bro) that lends itself to modular addition of new protocol parsers and event handling mechanisms. As an example we have shown an application of the technique to the IEC-60870-5-104 protocol and tested the anomaly detector with mixed results. The detection accuracy and false positive rate, as well as real-time response was adequate for 3 of our 4 created attacks. We also discovered some additional work that needs to be done to an existing protocol parser to extend its reach.
Lau, Stephan, Klick, Johannes, Arndt, Stephan, Roth, Volker.  2016.  POSTER: Towards Highly Interactive Honeypots for Industrial Control Systems. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :1823–1825.
Honeypots are a common tool to set intrusion alarms and to study attacks against computer systems. In order to be convincing, honeypots attempt to resemble actual systems that are in active use. Recently, researchers have begun to develop honeypots for programmable logic controllers (PLCs). The tools of which we are aware have limited functionality compared to genuine devices. Particularly, they do not support running actual PLC programs. In order to improve upon the interactive capabilities of PLC honeypots we set out to develop a simulator for Siemens S7-300 series PLCs. Our current prototype XPOT supports PLC program compilation and interpretation, the proprietary S7comm protocol and SNMP. While the supported feature set is not yet comprehensive, it is possible to program it using standard IDEs such as Siemens' TIA portal. Additionally, we emulate the characteristics of the network stack of our reference PLC in order to resist OS fingerprinting attempts using tools such as Nmap. Initial experiments with students whom we trained in PLC programming indicate that XPOT may resist cursory inspection but still fails against knowledgeable and suspicious adversaries. We conclude that high-interactive PLC honeypots need to support a fairly complete feature set of the genuine, simulated PLC.
2017-10-18
Ranganathan, Aanjhan, Ólafsdóttir, Hildur, Capkun, Srdjan.  2016.  SPREE: A Spoofing Resistant GPS Receiver. Proceedings of the 22Nd Annual International Conference on Mobile Computing and Networking. :348–360.

Global Positioning System (GPS) is used ubiquitously in a wide variety of applications ranging from navigation and tracking to modern smart grids and communication networks. However, it has been demonstrated that modern GPS receivers are vulnerable to signal spoofing attacks. For example, today it is possible to change the course of a ship or force a drone to land in a hostile area by simply spoofing GPS signals. Several countermeasures have been proposed in the past to detect GPS spoofing attacks. These counter-measures offer protection only against naive attackers. They are incapable of detecting strong attackers such as those capable of seamlessly taking over a GPS receiver, which is currently receiving legitimate satellite signals, and spoofing them to an arbitrary location. Also, there is no hardware platform that can be used to compare and evaluate the effectiveness of existing countermeasures in real-world scenarios. In this work, we present SPREE, which is, to the best of our knowledge, the first GPS receiver capable of detecting all spoofing attacks described in the literature. Our novel spoofing detection technique called auxiliary peak tracking enables detection of even a strong attacker capable of executing the seamless takeover attack. We implement and evaluate our receiver against three different sets of GPS signal traces: (i) a public repository of spoofing traces, (ii) signals collected through our own wardriving effort and (iii) using commercial GPS signal generators. Our evaluations show that SPREE constraints even a strong attacker (capable of seamless takeover attack) from spoofing the receiver to a location not more than 1 km away from its true location. This is a significant improvement over modern GPS receivers that can be spoofed to any arbitrary location. Finally, we release our implementation and datasets to the community for further research and development.

Wu, Jie, Liu, Jinglan, Hu, Xiaobo Sharon, Shi, Yiyu.  2016.  Privacy Protection via Appliance Scheduling in Smart Homes. Proceedings of the 35th International Conference on Computer-Aided Design. :106:1–106:6.

Smart grid, managed by intelligent devices, have demonstrated great potentials to help residential customers to optimally schedule and manage the appliances' energy consumption. Due to the fine-grained power consumption information collected by smart meter, the customers' privacy becomes a serious concern. Combined with the effects of fake guideline electricity price, this paper focuses an on-line appliance scheduling design to protect customers' privacy in a cost-effective way, while taking into account the influences of non-schedulable appliances' operation uncertainties. We formulate the problem by minimizing the expected sum of electricity cost and achieving acceptable privacy protection. Without knowledge of future electricity consumptions, an on-line scheduling algorithm is proposed based on the only current observations by using a stochastic dynamic programming technique. The simulation results demonstrate the effectiveness of the proposed algorithm using real-world data.

Conti, Mauro, Nati, Michele, Rotundo, Enrico, Spolaor, Riccardo.  2016.  Mind The Plug! Laptop-User Recognition Through Power Consumption. Proceedings of the 2Nd ACM International Workshop on IoT Privacy, Trust, and Security. :37–44.

The Internet of Things (IoT) paradigm, in conjunction with the one of smart cities, is pursuing toward the concept of smart buildings, i.e., “intelligent” buildings able to receive data from a network of sensors and thus to adapt the environment. IoT sensors can monitor a wide range of environmental features such as the energy consumption inside a building at fine-grained level (e.g., for a specific wall-socket). Some smart buildings already deploy energy monitoring in order to optimize the energy use for good purposes (e.g., to save money, to reduce pollution). Unfortunately, such measurements raise a significant amount of privacy concerns. In this paper, we investigate the feasibility of recognizing the pair laptop-user (i.e., a user using her own laptop) from the energy traces produced by her laptop. We design MTPlug, a framework that achieves this goal relying on supervised machine learning techniques as pattern recognition in multivariate time series. We present a comprehensive implementation of this system and run a thorough set of experiments. In particular, we collected data by monitoring the energy consumption of two groups of laptop users, some office employees and some intruders, for a total of 27 people. We show that our system is able to build an energy profile for a laptop user with accuracy above 80%, in less than 3.5 hours of laptop usage. To the best of our knowledge, this is the first research that assesses the feasibility of laptop users profiling relying uniquely on fine-grained energy traces collected using wall-socket smart meters.

Konstantinou, Charalambos, Maniatakos, Michail.  2016.  A Case Study on Implementing False Data Injection Attacks Against Nonlinear State Estimation. Proceedings of the 2Nd ACM Workshop on Cyber-Physical Systems Security and Privacy. :81–92.

Smart grid aims to improve control and monitoring routines to ensure reliable and efficient supply of electricity. The rapid advancements in information and communication technologies of Supervisory Control And Data Acquisition (SCADA) networks, however, have resulted in complex cyber physical systems. This added complexity has broadened the attack surface of power-related applications, amplifying their susceptibility to cyber threats. A particular class of system integrity attacks against the smart grid is False Data Injection (FDI). In a successful FDI attack, an adversary compromises the readings of grid sensors in such a way that errors introduced into estimates of state variables remain undetected. This paper presents an end-to-end case study of how to instantiate real FDI attacks to the Alternating Current (AC) –nonlinear– State Estimation (SE) process. The attack is realized through firmware modifications of the microprocessor-based remote terminal systems, falsifying the data transmitted to the SE routine, and proceeds regardless of perfect or imperfect knowledge of the current system state. The case study concludes with an investigation of an attack on the IEEE 14 bus system using load data from the New York Independent System Operator (NYISO).

Küçük, Kubilay Ahmet, Paverd, Andrew, Martin, Andrew, Asokan, N., Simpson, Andrew, Ankele, Robin.  2016.  Exploring the Use of Intel SGX for Secure Many-Party Applications. Proceedings of the 1st Workshop on System Software for Trusted Execution. :5:1–5:6.

The theoretical construct of a Trusted Third Party (TTP) has the potential to solve many security and privacy challenges. In particular, a TTP is an ideal way to achieve secure multiparty computation—a privacy-enhancing technique in which mutually distrusting participants jointly compute a function over their private inputs without revealing these inputs. Although there exist cryptographic protocols to achieve this, their performance often limits them to the two-party case, or to a small number of participants. However, many real-world applications involve thousands or tens of thousands of participants. Examples of this type of many-party application include privacy-preserving energy metering, location-based services, and mobile network roaming. Challenging the notion that a trustworthy TTP does not exist, recent research has shown how trusted hardware and remote attestation can be used to establish a sufficient level of assurance in a real system such that it can serve as a trustworthy remote entity (TRE). We explore the use of Intel SGX, the most recent and arguably most promising trusted hardware technology, as the basis for a TRE for many-party applications. Using privacy-preserving energy metering as a case study, we design and implement a prototype TRE using SGX, and compare its performance to a previous system based on the Trusted Platform Module (TPM). Our results show that even without specialized optimizations, SGX provides comparable performance to the optimized TPM system, and therefore has significant potential for large-scale many-party applications.

Ren, Wenyu, Nahrstedt, Klara, Yardley, Tim.  2016.  Operation-level Traffic Analyzer Framework for Smart Grid. Proceedings of the Symposium and Bootcamp on the Science of Security. :112–114.

The Smart Grid control systems need to be protected from internal attacks within the perimeter. In Smart Grid, the Intelligent Electronic Devices (IEDs) are resource-constrained devices that do not have the ability to provide security analysis and protection by themselves. And the commonly used industrial control system protocols offer little security guarantee. To guarantee security inside the system, analysis and inspection of both internal network traffic and device status need to be placed close to IEDs to provide timely information to power grid operators. For that, we have designed a unique, extensible and efficient operation-level traffic analyzer framework. The timing evaluation of the analyzer overhead confirms efficiency under Smart Grid operational traffic.

Han, Wenlin, Xiao, Yang.  2016.  FNFD: A Fast Scheme to Detect and Verify Non-Technical Loss Fraud in Smart Grid. Proceedings of the 2016 ACM International on Workshop on Traffic Measurements for Cybersecurity. :24–34.

Non-Technical Loss (NTL) fraud is a very common fraud in power systems. In traditional power grid, energy theft, via meter tampering, is the main form of NTL fraud. With the rise of Smart Grid, adversaries can take advantage of two-way communication to commit NTL frauds by meter manipulation or network intrusion. Previous schemes were proposed to detect NTL frauds but are not efficient. In this paper, we propose a Fast NTL Fraud Detection and verification scheme (FNFD). FNFD is based on Recursive Least Square (RLS) to model adversary behavior. Experimental results show that FNFD outperforms existing schemes in terms of efficiency and overhead.

2017-10-13
Costanzo, David, Shao, Zhong, Gu, Ronghui.  2016.  End-to-end Verification of Information-flow Security for C and Assembly Programs. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. :648–664.

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly; we verify all of the code, regardless of language.

Mäki, Petteri, Rauti, Sampsa, Hosseinzadeh, Shohreh, Koivunen, Lauri, Leppänen, Ville.  2016.  Interface Diversification in IoT Operating Systems. Proceedings of the 9th International Conference on Utility and Cloud Computing. :304–309.

With the advancement of Internet in Things (IoT) more and more "things" are connected to each other through the Internet. Due to the fact that the collected information may contain personal information of the users, it is very important to ensure the security of the devices in IoT. Diversification is a promising technique that protects the software and devices from harmful attacks and malware by making interfaces unique in each separate system. In this paper we apply diversification on the interfaces of IoT operating systems. To this aim, we introduce the diversification in post-compilation and linking phase of the software life-cycle, by shuffling the order of the linked objects while preserving the semantics of the code. This approach successfully prevents malicious exploits from producing adverse effects in the system. Besides shuffling, we also apply library symbol diversification method, and construct needed support for it e.g. into the dynamic loading phase. Besides studying and discussing memory layout shuffling and symbol diversification as a security measures for IoT operating systems, we provide practical implementations for these schemes for Thingsee OS and Raspbian operating systems and test these solutions to show the feasibility of diversification in IoT environments.

Weichslgartner, Andreas, Wildermann, Stefan, Götzfried, Johannes, Freiling, Felix, Glaß, Michael, Teich, Jürgen.  2016.  Design-Time/Run-Time Mapping of Security-Critical Applications in Heterogeneous MPSoCs. Proceedings of the 19th International Workshop on Software and Compilers for Embedded Systems. :153–162.

Different applications concurrently running on modern MPSoCs can interfere with each other when they use shared resources. This interference can cause side channels, i.e., sources of unintended information flow between applications. To prevent such side channels, we propose a hybrid mapping methodology that attempts to ensure spatial isolation, i.e., a mutually-exclusive allocation of resources to applications in the MPSoC. At design time and as a first step, we compute compact and connected application mappings (called shapes). In a second step, run-time management uses this information to map multiple spatially segregated shapes to the architecture. We present and evaluate a (fast) heuristic and an (exact) SAT-based mapper, demonstrating the viability of the approach.