Visible to the public Confinement 2015

SoS Newsletter- Advanced Book Block


SoS Logo



In photonics, confinement is important to loss avoidance. In quantum theory, it relates to energy levels. The articles cited here cover both concepts and were presented or published in 2015. Containment is important in the contexts of cyber-physical systems, privacy, resiliency, and composability. 

Ed Novak, Yutao Tang, Zijiang Hao, Qun Li, Yifan Zhang; “Physical Media Covert Channels on Smart Mobile Devices,” UbiComp ’15, Proceedings of the 2015 ACM International Joint Conference on Pervasive and Ubiquitous Computing, September 2015, Pages 367–378. doi:10.1145/2750858.2804253
Abstract: In recent years mobile smart devices such as tablets and smartphones have exploded in popularity. We are now in a world of ubiquitous smart devices that people rely on daily and carry everywhere. This is a fundamental shift for computing in two ways. Firstly, users increasingly place unprecedented amounts of sensitive information on these devices, which paints a precarious picture. Secondly, these devices commonly carry many physical world interfaces. In this paper, we propose information leakage malware, specifically designed for mobile devices, which uses covert channels over physical “real-world” media, such as sound or light. This malware is stealthy; able to circumvent current, and even state-of-the-art defenses to enable attacks including privilege escalation, and information leakage. We go on to present a defense mechanism, which balances security with usability to stop these attacks.
Keywords: covert channel, physical media, privacy, security, sensors, smart mobile device (ID#: 15-6954)


Danfeng Zhang, Yao Wang, G. Edward Suh, Andrew C. Myers; “A Hardware Design Language for Timing-Sensitive Information-Flow Security,” ASPLOS ’15, Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, March 2015, Pages 503–516. doi:10.1145/2775054.2694372
Abstract: Information security can be compromised by leakage via low-level hardware features. One recently prominent example is cache probing attacks, which rely on timing channels created by caches. We introduce a hardware design language, SecVerilog, which makes it possible to statically analyze information flow at the hardware level. With SecVerilog, systems can be built with verifiable control of timing channels and other information channels. SecVerilog is Verilog, extended with expressive type annotations that enable precise reasoning about information flow. It also comes with rigorous formal assurance: we prove that SecVerilog enforces timing-sensitive noninterference and thus ensures secure information flow. By building a secure MIPS processor and its caches, we demonstrate that SecVerilog makes it possible to build complex hardware designs with verified security, yet with low overhead in time, space, and HW designer effort.
Keywords: dependent types, hardware description language, information flow control, timing channels (ID#: 15-6955)


C. Louison, F. Ferlay, D. Keller, D. Mestre; “Vibrotactile Feedback for Collision Awareness,” British HCI ’15, Proceedings of the 2015 British HCI Conference, July 2015, Pages 277–278. doi:10.1145/2783446.2783609
Abstract: Magnetic Confinement Fusion machines called tokamak (e.g. ITER and WEST projects), as well as many industrial projects, require a high integration level in a confined volume. The feasibility of installation and maintenance by an operator has to be considered in the early stages of the design. Virtual reality technologies have opened new perspectives and solutions to take into account assembly and maintenance constraints, using virtual mock-ups. In our applications, the human factor takes an important role. Since the operator interacts in a very tight and confined environment, he has to pay attention to his whole body relative to the virtual environment, in the absence of haptic feedback. In this context, enriched sensorial information, called “collision awareness feedback”, must be defined, to favour an appropriate operator’s spatial behavior with respect to the environment. In this paper, we present a preliminary study, testing the effect of vibrotactile feedback in a simple tracking task, compared to a pure visual feedback.
Keywords: assembly task, collision awareness, tactile sense, vibrotactile, virtual human, virtual reality (ID#: 15-6956)


Petr Hosek, Cristian Cadar; “VARAN the Unbelievable: An Efficient N-version Execution Framework,” ASPLOS ’15, Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, March 2015, Pages 339–353. doi:10.1145/2775054.2694390
Abstract: With the widespread availability of multi-core processors, running multiple diversified variants or several different versions of an application in parallel is becoming a viable approach for increasing the reliability and security of software systems. The key component of such N-version execution (NVX) systems is a runtime monitor that enables the execution of multiple versions in parallel. Unfortunately, existing monitors impose either a large performance overhead or rely on intrusive kernel-level changes. Moreover, none of the existing solutions scales well with the number of versions, since the runtime monitor acts as a performance bottleneck.  In this paper, we introduce Varan, an NVX framework that combines selective binary rewriting with a novel event-streaming architecture to significantly reduce performance overhead and scale well with the number of versions, without relying on intrusive kernel modifications.  Our evaluation shows that Varan can run NVX systems based on popular C10k network servers with only a modest performance overhead, and can be effectively used to increase software reliability using techniques such as transparent failover, live sanitization and multi-revision execution.
Keywords: N-version execution, event streaming, live sanitization, multi-revision execution, record-replay, selective binary rewriting, transparent failover (ID#: 15-6957)


Adam Procter, William L. Harrison, Ian Graves, Michela Becchi, Gerard Allwein; “Semantics Driven Hardware Design, Implementation, and Verification with ReWire,” LCTES’15, Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems 2015, CD-ROM, June 2015, Article No. 13. doi:10.1145/2670529.2754970
Abstract: There is no such thing as high assurance without high assurance hardware. High assurance hardware is essential, because any and all high assurance systems ultimately depend on hardware that conforms to, and does not undermine, critical system properties and invariants. And yet, high assurance hardware development is stymied by the conceptual gap between formal methods and hardware description languages used by engineers. This paper presents ReWire, a functional programming language providing a suitable foundation for formal verification of hardware designs, and a compiler for that language that translates high-level, semantics-driven designs directly into working hardware. ReWire’s design and implementation are presented, along with a case study in the design of a secure multicore processor, demonstrating both ReWire’s expressiveness as a programming language and its power as a framework for formal, high-level reasoning about hardware systems.
Keywords: (not provided) (ID#: 15-6958)


Po-Hsun Wu, Mark Po-Hung Lin, Xin Li, Tsung-Yi Ho; “Common-Centroid FinFET Placement Considering the Impact of Gate Misalignment,” ISPD ’15, Proceedings of the 2015 Symposium on International Symposium on Physical Design, March 2015, Pages 25–31. doi:10.1145/2717764.2717769
Abstract: The FinFET technology has been regarded as a better alternative among different device technologies at 22nm node and beyond due to more effective channel control and lower power consumption. However, the gate misalignment problem resulting from process variation based on the FinFET technology becomes even severer compared with the conventional planar CMOS technology. Such misalignment may increase the threshold voltage and decrease the drain current of a single transistor. When applying the FinFET technology to analog circuit design, the variation of drain currents will destroy the current matching among transistors and degrade the circuit performance. In this paper, we present the first FinFET placement technique for analog circuits considering the impact of gate misalignment together with systematic and random mismatch. Experimental results show that the proposed algorithms can obtain an optimized common-centroid FinFET placement with much better current matching.
Keywords: analog placement, common centroid, finfet, gate misalignment (ID#: 15-6959)


Alejandro Russo; “Functional Pearl: Two Can Keep a Secret, if One of Them Uses Haskell,” ICFP 2015, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, August 2015, Pages 280–288. doi:10.1145/2784731.2784756
Abstract: For several decades, researchers from different communities have independently focused on protecting confidentiality of data. Two distinct technologies have emerged for such purposes: Mandatory Access Control (MAC) and Information-Flow Control (IFC)—the former belonging to operating systems (OS) research, while the latter to the programming languages community. These approaches restrict how data gets propagated within a system in order to avoid information leaks. In this scenario, Haskell plays a unique privileged role: it is able to protect confidentiality via libraries. This pearl presents a monadic API which statically protects confidentiality even in the presence of advanced features like exceptions, concurrency, and mutable data structures. Additionally, we present a mechanism to safely extend the library with new primitives, where library designers only need to indicate the read and write effects of new operations.
Keywords: information-flow control, library, mandatory access control, security (ID#: 15-6960)


Mehdi Bagherzadeh, Hridesh Rajan; “Panini: A Concurrent Programming Model for Solving Pervasive and Oblivious Interference,” MODULARITY 2015, Proceedings of the 14th International Conference on Modularity, March 2015, Pages 93–108. doi:10.1145/2724525.2724568
Abstract: Modular reasoning about concurrent programs is complicated by the possibility of interferences happening between any two instructions of a task (pervasive interference), and these interferences not giving out any information about the behaviors of potentially interfering concurrent tasks (oblivious interference). Reasoning about a concurrent program would be easier if a programmer modularly and statically (1) knows precisely the program points at which interferences may happen (sparse interference), and (2) has some insights into behaviors of potentially interfering tasks at these points (cognizant interference). In this work we present Panini, a core concurrent calculus which guarantees sparse interference, by controlling sharing among concurrent tasks, and cognizant interference, by controlling dynamic name bindings and accessibility of states of tasks. Panini promotes capsule-oriented programming whose concurrently running capsules own their states, communicate by asynchronous invocations of their procedures and dynamically transfer ownership. Panini limits sharing among two capsules to other capsules and futures, limits accessibility of a capsule states to only through its procedures and dispatches a procedure invocation on the static type of its receiver capsule. We formalize Panini, present its semantics and illustrate how its interference model, using behavioral contracts, enables Hoare-style modular reasoning about concurrent programs with interference.
Keywords: Pervasive interference, capsule-oriented programming, message passing, modular reasoning, oblivious interference (ID#: 15-6961)


Yuanzhong Xu, Emmett Witchel; “Maxoid: Transparently Confining Mobile Applications with Custom Views of State,” EuroSys ’15, Proceedings of the Tenth European Conference on Computer Systems, April 2015, Article No. 26. doi:10.1145/2741948.2741966
Abstract: We present Maxoid, a system that allows an Android app to process its sensitive data by securely invoking other, untrusted apps. Maxoid provides secrecy and integrity for both the invoking app and the invoked app. For each app, Maxoid presents custom views of private and public state (files and data in content providers) to transparently redirect unsafe data flows and minimize disruption. Maxoid supports unmodified apps with full security guarantees, and also introduces new APIs to improve usability. We show that Maxoid can improve security for popular Android apps with minimal performance overheads.
Keywords: (not provided) (ID#: 15-6962)


Stefan Haar, Salim Perchy, Camilo Rueda, Frank Valencia; “An Algebraic View of Space/Belief and Extrusion/Utterance for Concurrency/Epistemic Logic,” PPDP ’15, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, July 2015, Pages 161–172. doi:10.1145/2790449.2790520
Abstract: We enrich spatial constraint systems with operators to specify information and processes moving from a space to another. We shall refer to these news structures as spatial constraint systems with extrusion. We shall investigate the properties of this new family of constraint systems and illustrate their applications. From a computational point of view the new operators provide for process/information extrusion, a central concept in formalisms for mobile communication. From an epistemic point of view extrusion corresponds to a notion we shall call utterance; a piece of information that an agent communicates to others but that may be inconsistent with the agent’s beliefs. Utterances can then be used to express instances of epistemic notions, which are common place in social media, such as hoaxes or intentional lies. Spatial constraint systems with extrusion can be seen as complete Heyting algebras equipped with maps to account for spatial and epistemic specifications.
Keywords: extrusion, lies, mobility, social networks, space, utterance (ID#: 15-6963)


Qi Hu, Peng Liu, Michael C. Huang, Xiang-Hui Xie; “Exploiting Transmission Lines on Heterogeneous Networks-on-Chip to Improve the Adaptivity and Efficiency of Cache Coherence,” NOCS ’15, Proceedings of the 9th International Symposium on Networks-on-Chip, September 2015, Article No. 14. doi:10.1145/2786572.2786576
Abstract: Emerging heterogeneous interconnects have shown lower latency and higher throughput, which can improve the efficiency of communication and create new opportunities for memory system designs. In this paper, transmission lines are employed as a latency-optimized network and combined with a packet-switched network to create heterogeneous interconnects improving the efficiencies of on-chip communication and cache coherence. We take advantage of this heterogeneous interconnect design, and keep cache coherence adaptively based on data locality. Different type of messages are adaptively directed through selected medium of the heterogeneous interconnects to enhance cache coherence effectiveness. Compared with a state-of-the-art coherence mechanism, the proposed technique can reduce the coherence overhead by 24%, reduce the network energy consumption by 35%, and improve the system performance by 25% on a 64-core system.
Keywords: Cache coherence, heterogeneous networks-on-chip (ID#: 15-6964)


Yajin Zhou, Kunal Patel, Lei Wu, Zhi Wang, Xuxian Jiang; “Hybrid User-level Sandboxing of Third-party Android Apps,” ASIACCS ’15, Proceedings of the 10th ACM Symposium on Information, Computer and Communications Security, April 2015, Pages 19–30. doi:10.1145/2714576.2714598
Abstract: Users of Android phones increasingly entrust personal information to third-party apps. However, recent studies reveal that many apps, even benign ones, could leak sensitive information without user awareness or consent. Previous solutions either require to modify the Android framework thus significantly impairing their practical deployment, or could be easily defeated by malicious apps using a native library.  In this paper, we propose AppCage, a system that thoroughly confines the run-time behavior of third-party Android apps without requiring framework modifications or root privilege. AppCage leverages two complimentary user-level sandboxes to interpose and regulate an app’s access to sensitive APIs. Specifically, dex sandbox hooks into the app’s Dalvik virtual machine instance and redirects each sensitive framework API to a proxy which strictly enforces the user-defined policies, and native sandbox leverages software fault isolation to prevent the app’s native libraries from directly accessing the protected APIs or subverting the dex sandbox. We have implemented a prototype of AppCage. Our evaluation shows that AppCage can successfully detect and block attempts to leak private information by third-party apps, and the performance overhead caused by AppCage is negligible for apps without native libraries and minor for apps with them.
Keywords: android, dalvik hooking, software fault isolation (ID#: 15-6965)


Elena Cardillo, Maria Teresa Chiaravalloti, Erika Pasceri; “Assessing ICD-9-CM and ICPC-2 Use in Primary Care. An Italian Case Study,” DH ’15, Proceedings of the 5th International Conference on Digital Health 2015, May 2015, Pages 95–102. doi:10.1145/2750511.2750525
Abstract: Controlled vocabularies and standardized coding systems play a fundamental role in the healthcare domain. The International Classification of Diseases (ICD) is one of the most widely used classification systems for clinical problems and procedures. In Italy the 9th revision of the standard is used and recommended in primary care for encoding prescription documents. This paper describes a statistical and terminological study to assess ICD-9-CM use in primary care and its comparison to the International Classification of Primary Care (ICPC), specifically designed for primary care. The study has been conducted by analyzing the clinical records of about 199,000 patients provided by a set of 166 General Practitioners (GPs) in different Italian areas. The analysis has been based on several techniques for detecting coding practice and errors, like natural language processing and text-similarity comparison. Results showed that the selected GPs do not fully exploit the diseases and procedures descriptive capabilities of ICD-9-CM due to its complexity. Furthermore, compared to ICPC-2, it resulted less feasible in the primary care setting, particularly for the high granularity of the structure and for the lack of reasons for encounters.
Keywords: classification systems, e-health, primary care, terminology icd icpc (ID#: 15-6966)


Sophia Drossopoulou, James Noble, Mark S. Miller; “Swapsies on the Internet: First Steps towards Reasoning about Risk and Trust in an Open World,” PLAS’15, Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, July 2015, Pages 2–15. doi:10.1145/2786558.2786564
Abstract: Contemporary open systems use components developed by many different parties, linked together dynamically in unforeseen constellations. Code needs to live up to strict security specifications: it has to ensure the correct functioning of its objects when they collaborate with external objects which may be malicious.  In this paper we propose specifications that model risk and trust in such open systems. We specify Miller, Van Cutsem, and Tulloh’s escrow exchange example, and discuss the meaning of such a specification. We argue informally that the code satisfies its specification.
Keywords: (not provided) (ID#: 15-6967)


Florian Floyd Mueller, Joe Marshall, Rohit Ashok Khot, Stina Nylander, Jakob Tholander; “Understanding Sports-HCI by Going Jogging at CHI,” CHI EA ’15, Proceedings of the 33rd Annual ACM Conference Extended Abstracts on Human Factors in Computing Systems, April 2015, Pages 869–872. doi:10.1145/2702613.2727688
Abstract: More and more technologies are emerging that aim to support sports activities, for example there are jogging apps, cycling computers and quadcopters for sportspeople to videorecord their actions. These new technologies appear to become more and more popular, yet interaction design knowledge how to support the associated exertion experiences is still limited. In order to bring practitioners and academics interested in sports-HCI together and examine the topic “in the wild”, we propose to go outside and jog around the CHI venue while using and discussing some of these new technologies. The goal is to investigate and shape the future of the field of sports-HCI.
Keywords: exercise, exertion, sport (ID#: 15-6968)


H.-S. Philip Wong, He Yi, Maryann Tung, Kye Okabe; “Physical Layout Design of Directed Self-Assembly Guiding Alphabet for IC Contact Hole/via Patterning,” ISPD ’15, Proceedings of the 2015 Symposium on International Symposium on Physical Design, March 2015, Pages 65–66.  doi:10.1145/2717764.2723574
Abstract: The continued scaling of feature size has brought increasingly significant challenges to conventional optical lithography.[1-3] The rising cost and limited resolution of current lithography technologies have opened up opportunities for alternative patterning approaches. Among the emerging patterning approaches, block copolymer self-assembly for device fabrication has been envisioned for over a decade. Block copolymer DSA is a result of spontaneous microphase separation of block copolymer films, forming periodic microdomains including cylinders, spheres, and lamellae, in the same way that snowflakes and clamshells are formed in nature - by self-assembly due to forces of nature (Fig. 1a). DSA can generate closely packed and well controlled sub-20 nm features with low cost and high throughput, therefore stands out among other emerging lithographic solutions, including extreme ultraviolet lithography (EUV), electron beam lithography (e-beam), and multiple patterning lithography (MPL).[2;6]  Previous research has shown a high degree of dimensional control of the self-assembled features over large areas with long range ordering and periodic structures.[5; 6] The exquisite dimensional control at nanometer-scale feature sizes is one of the most attractive properties of block copolymer self-assembly. At the same time, device and circuit fabrication for the semiconductor industry requires accurate placement of desired features at irregular positions on the chip. The need to coax the self-assembled features into circuit layout friendly location is a roadblock for introducing self-assembly into semiconductor manufacturing. Directed self-assembly (DSA) and the use of topography to direct the self-assembly (graphoepitaxy) have shown great potential in overcoming the current lithography limits.[4]  Recognizing that typical circuit layouts do not require long range order, we adopt a lithography sub-division approach akin to double-patterning and spacer patterning, using small guiding topographical templates. Guiding topographical templates with sizes of the order of the natural pitch of the block copolymer can effectively guide the self-assembly of block polymer (Fig. 1b-c). Therefore, circuit contact hole patterns can be placed at arbitrary location by first patterning a coarse guiding template using conventional lithography.[7; 8] This procedure enables generating a higher resolution feature at a location determined by the coarse lithographic pattern. The size and registration of the features are determined by parameters of the template as well as the block copolymer itself.  Using this technique, we have proposed a general template design strategy that relates the block copolymer material properties to the target technology node requirements, and demonstrated contact hole patterning at the technology node from 22 nm to 7 nm, for both memory circuits and random logic circuits.[11] The critical dimension of DSA patterns is highly uniform, with their position controlled precisely. As technology scales down, the contact/via density scales up, which simultaneously opens the possibility of using multiple-hole DSA patterns for contact hole patterning and brings in the challenge of printing guiding templates at a small pitch. Using DSA for patterning IC contacts requires further knowledge of the placement of contacts in an IC layout, as the placement of contacts in the IC layout determines the shape and size of the required templates.  We hypothesize that there exists a limited set of guiding templates analogous to the letters of an alphabet that can cover all the possible contact hole patterns of a full chip contact layer.[12] This alphabet approach would significantly simplify DSA contact hole patterning when the total number of letters of the alphabet is small and would allow us to focus on fully characterizing only the design spaces for the letters of the alphabet. By positioning these letters in various locations we would be able to pattern the full chip contact layer in the same way that the 26 letters of the English alphabet is sufficient to compose an English newspaper. Some of the most basic letters, such as circular templates for 1-hole DSA patterns and elliptical templates for 2- and 3-hole DSA patterns, have been studied extensively.[12] To establish a complete alphabet, though, requires the examination of the entire standard cell library, as well as the optimization of the layout to further reduce the number of letters in the alphabet.[5]  The broad community of DSA researchers has made tremendous progress in the past few years. However to make DSA fully qualified for large-scale semiconductor manufacturing, technical issues such as defectivity reduction and overlay optimization must be solved. While many researchers are developing new block copolymer materials for better chemical properties, there remains more works to be accomplished from the circuit and system design level, including IC layouts optimization for the improvement of DSA process yield and DSA full-chip hotspot detection. Challenges such as optimizing and tuning the template design based on overlay, defectivity, and lithography requirements will need to be further investigated in order for practical implementation in industry.
Keywords: block copolymer, contact hole, directed self-assembly, layout design, lithography (ID#: 15-6969)


Yehuda Afek, Anat Bremler-Barr, Shir Landau Feibish, Liron Schiff; “Sampling and Large Flow Detection in SDN,” SIGCOMM ’15, Proceedings of the 2015 ACM Conference on Special Interest Group on Data Communication, August 2015, Pages 345–346. doi:10.1145/2785956.2790009
Abstract: (not provided)
Keywords: heavy hitters, network monitoring, software defined networks (ID#: 15-6970)


Yasmine Badr, Andres Torres, Puneet Gupta; “Mask Assignment and Synthesis of DSA-MP Hybrid Lithography for sub-7nm Contacts/Vias,” DAC ’15, Proceedings of the 52nd Annual Design Automation Conference, June 2015, Article No. 70. doi:10.1145/2744769.2744868
Abstract: Integrating Directed Self Assembly (DSA) and Multiple Patterning (MP) is an attractive option for printing contact and via layers for sub-7nm process nodes. In the DSA-MP hybrid process, an optimized decomposition algorithm is required to perform the MP mask assignment while considering the DSA advantages and limitations. In this paper, we present an optimal Integer Linear Programming (ILP) formulation for the simultaneous DSA grouping and MP decomposition problem for contacts and vias. Then we propose a heuristic and develop an efficient algorithm for solving the same problem. In comparison to the optimal ILP results, the proposed algorithm is 197x faster and results in 16.3% more violations. The proposed algorithm produces 56% fewer violations than the sequential approaches which perform DSA grouping followed by MP decomposition and vice versa.
Keywords: DSA, MP, Moore’s law, decomposition, directed self assembly, multiple patterning, technology (ID#: 15-6971)


Xin Chen, Sencun Zhu; “DroidJust: Automated Functionality-Aware Privacy Leakage Analysis for Android Applications,” WiSec ’15, Proceedings of the 8th ACM Conference on Security & Privacy in Wireless and Mobile Networks, June 2015, Article No. 5. doi:10.1145/2766498.2766507
Abstract: Android applications (apps for short) can send out users’ sensitive information against users’ intention. Based on the stats from Genome and Mobile-Sandboxing, 55.8% and 59.7% Android malware families feature privacy leakage. Prior approaches to detecting privacy leakage on smartphones primarily focused on the discovery of sensitive information flows. However, Android apps also send out users’ sensitive information for legitimate functions. Due to the fuzzy nature of the privacy leakage detection problem, we formulate it as a justification problem, which aims to justify if a sensitive information transmission in an app serves any purpose, either for intended functions of the app itself or for other related functions. This formulation makes the problem more distinct and objective, and therefore more feasible to solve than before. We propose DroidJust, an automated approach to justifying an app’s sensitive information transmission by bridging the gap between the sensitive information transmission and application functions. We also implement a prototype of DroidJust and evaluate it with over 6000 Google Play apps and over 300 known malware collected from VirusTotal. Our experiments show that our tool can effectively and efficiently analyze Android apps w.r.t their sensitive information flows and functionalities, and can greatly assist in detecting privacy leakage.
Keywords: Android security, privacy leakage detection, static taint analysis (ID#: 15-6972)


Articles listed on these pages have been found on publicly available internet pages and are cited with links to those pages. Some of the information included herein has been reprinted with permission from the authors or data repositories. Direct any requests via Email to for removal of the links or modifications to specific citations. Please include the ID# of the specific citation in your correspondence.