Visible to the public Biblio

Found 675 results

Filters: First Letter Of Last Name is O  [Clear All Filters]
2017-08-02
Gao, Ning, Bagdouri, Mossaab, Oard, Douglas W..  2016.  Pearson Rank: A Head-Weighted Gap-Sensitive Score-Based Correlation Coefficient. Proceedings of the 39th International ACM SIGIR Conference on Research and Development in Information Retrieval. :941–944.

One way of evaluating the reusability of a test collection is to determine whether removing the unique contributions of some system would alter the preference order between that system and others. Rank correlation measures such as Kendall's tau are often used for this purpose. Rank correlation measures are appropriate for ordinal measures in which only preference order is important, but many evaluation measures produce system scores in which both the preference order and the magnitude of the score difference are important. Such measures are referred to as interval. Pearson's rho offers one way in which correlation can be computed over results from an interval measure such that smaller errors in the gap size are preferred. When seeking to improve over existing systems, we care the most about comparisons among the best systems. For that purpose we prefer head-weighed measures such as tau\_AP, which is designed for ordinal data. No present head weighted measure fully leverages the information present in interval effectiveness measures. This paper introduces such a measure, referred to as Pearson Rank.

Moran, Sean, McCreadie, Richard, Macdonald, Craig, Ounis, Iadh.  2016.  Enhancing First Story Detection Using Word Embeddings. Proceedings of the 39th International ACM SIGIR Conference on Research and Development in Information Retrieval. :821–824.

In this paper we show how word embeddings can be used to increase the effectiveness of a state-of-the art Locality Sensitive Hashing (LSH) based first story detection (FSD) system over a standard tweet corpus. Vocabulary mismatch, in which related tweets use different words, is a serious hindrance to the effectiveness of a modern FSD system. In this case, a tweet could be flagged as a first story even if a related tweet, which uses different but synonymous words, was already returned as a first story. In this work, we propose a novel approach to mitigate this problem of lexical variation, based on tweet expansion. In particular, we propose to expand tweets with semantically related paraphrases identified via automatically mined word embeddings over a background tweet corpus. Through experimentation on a large data stream comprised of 50 million tweets, we show that FSD effectiveness can be improved by 9.5% over a state-of-the-art FSD system.

2017-07-24
Jakobsen, Sune K., Orlandi, Claudio.  2016.  How To Bootstrap Anonymous Communication. Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science. :333–344.

We ask whether it is possible to anonymously communicate a large amount of data using only public (non-anonymous) communication together with a small anonymous channel. We think this is a central question in the theory of anonymous communication and to the best of our knowledge this is the first formal study in this direction. Towards this goal, we introduce the novel concept of anonymous steganography: think of a leaker Lea who wants to leak a large document to Joe the journalist. Using anonymous steganography Lea can embed this document in innocent looking communication on some popular website (such as cat videos on YouTube or funny memes on 9GAG). Then Lea provides Joe with a short decoding key dk which, when applied to the entire website, recovers the document while hiding the identity of Lea among the large number of users of the website. Our contributions include: Introducing and formally defining anonymous steganography, A construction showing that anonymous steganography is possible (which uses recent results in circuits obfuscation), A lower bound on the number of bits which are needed to bootstrap anonymous communication.

2017-06-27
Obermaier, Johannes, Hutle, Martin.  2016.  Analyzing the Security and Privacy of Cloud-based Video Surveillance Systems. Proceedings of the 2Nd ACM International Workshop on IoT Privacy, Trust, and Security. :22–28.

In the area of the Internet of Things, cloud-based camera surveillance systems are ubiquitously available for industrial and private environments. However, the sensitive nature of the surveillance use case imposes high requirements on privacy/confidentiality, authenticity, and availability of such systems. In this work, we investigate how currently available mass-market camera systems comply with these requirements. Considering two attacker models, we test the cameras for weaknesses and analyze for their implications. We reverse-engineered the security implementation and discovered several vulnerabilities in every tested system. These weaknesses impair the users' privacy and, as a consequence, may also damage the camera system manufacturer's reputation. We demonstrate how an attacker can exploit these vulnerabilities to blackmail users and companies by denial-of-service attacks, injecting forged video streams, and by eavesdropping private video data - even without physical access to the device. Our analysis shows that current systems lack in practice the necessary care when implementing security for IoT devices.

Ravenet, Brian, Bevacqua, Elisabetta, Cafaro, Angelo, Ochs, Magalie, Pelachaud, Catherine.  2016.  Perceiving Attitudes Expressed Through Nonverbal Behaviors in Immersive Virtual Environments. Proceedings of the 9th International Conference on Motion in Games. :175–180.

Virtual Reality and immersive experiences, which allow players to share the same virtual environment as the characters of a virtual world, have gained more and more interest recently. In order to conceive these immersive virtual worlds, one of the challenges is to give to the characters that populate them the ability to express behaviors that can support the immersion. In this work, we propose a model capable of controlling and simulating a conversational group of social agents in an immersive environment. We describe this model which has been previously validated using a regular screen setting and we present a study for measuring whether users recognized the attitudes expressed by virtual agents through the realtime generated animations of nonverbal behavior in an immersive setting. Results mirrored those of the regular screen setting thus providing further insights for improving players experiences by integrating them into immersive simulated group conversations with characters that express different interpersonal attitudes.

2017-06-05
Schordan, Markus, Oppelstrup, Tomas, Jefferson, David, Barnes, Jr., Peter D., Quinlan, Dan.  2016.  Automatic Generation of Reversible C++ Code and Its Performance in a Scalable Kinetic Monte-Carlo Application. Proceedings of the 2016 Annual ACM Conference on SIGSIM Principles of Advanced Discrete Simulation. :111–122.

The fully automatic generation of code that establishes the reversibility of arbitrary C/C++ code has been a target of research and engineering for more than a decade as reverse computation has become a central notion in large scale parallel discrete event simulation (PDES). The simulation models that are implemented for PDES are of increasing complexity and size and require various language features to support abstraction, encapsulation, and composition when building a simulation model. In this paper we focus on parallel simulation models that are written in C++ and present an approach and an evaluation for a fully automatically generated reversible code for a kinetic Monte-Carlo application implemented in C++. Although a significant runtime overhead is introduced with our technique, the assurance that the reverse code is generated automatically and correctly, is an enormous win that allows simulation model developers to write forward event code using the entire C++ language, and have that code automatically transformed into reversible code to enable parallel execution with the Rensselaer's Optimistic Simulation System (ROSS).

Li, Wenjie, Qin, Zheng, Yin, Hui, Li, Rui, Ou, Lu, Li, Heng.  2016.  An Approach to Rule Placement in Software-Defined Networks. Proceedings of the 19th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems. :115–118.

Software-Defined Networks (SDN) is a trend of research in networks. Rule placement, a common operation for network administrators, has become more complicated due to the capacity limitation of devices in which the large number of rules are deployed. Prior works on rule placement mostly consider the influence on rule placement incurred by the rules in a single device. However, the position relationships between neighbor devices have influences on rule placement. Our basic idea is to classify the position relationships into two categories: the serial relationship and the parallel relationship, and we present a novel strategy for rule placement based on the two different position relationships. There are two challenges of implementing our strategies: to check whether a rule is contained by a rule set or not and to check whether a rule can be merged by other rules or not.To overcome the challenges, we propose a novel data structure called OPTree to represent the rules, which is convenient to check whether a rule is covered by other rules. We design the insertion algorithm and search algorithm for OPTree. Extensive experiments show that our approach can effectively reduce the number of rules while ensuring placed rules work. On the other hand, the experimental results also demonstrate that it is necessary to consider the position relationships between neighbor devices when placing rules.

Cox, Jr., Jacob H., Clark, Russell J., Owen, III, Henry L..  2016.  Leveraging SDN to Improve the Security of DHCP. Proceedings of the 2016 ACM International Workshop on Security in Software Defined Networks & Network Function Virtualization. :35–38.

Current State of the art technologies for detecting and neutralizing rogue DHCP servers are tediously complex and prone to error. Network operators can spend hours (even days) before realizing that a rogue server is affecting their network. Additionally, once network operators suspect that a rogue server is active on their network, even more hours can be spent finding the server's MAC address and preventing it from affecting other clients. Not only are such methods slow to eliminate rogue servers, they are also likely to affect other clients as network operators shutdown services while attempting to locate the server. In this paper, we present Network Flow Guard (NFG), a simple security application that utilizes the software defined networking (SDN) paradigm of programmable networks to detect and disable rogue servers before they are able to affect network clients. Consequently, the key contributions of NFG are its modular approach and its automated detection/prevention of rogue DHCP servers, which is accomplished with little impact to network architecture, protocols, and network operators.

Kellaris, Georgios, Kollios, George, Nissim, Kobbi, O'Neill, Adam.  2016.  Generic Attacks on Secure Outsourced Databases. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :1329–1340.

Recently, various protocols have been proposed for securely outsourcing database storage to a third party server, ranging from systems with "full-fledged" security based on strong cryptographic primitives such as fully homomorphic encryption or oblivious RAM, to more practical implementations based on searchable symmetric encryption or even on deterministic and order-preserving encryption. On the flip side, various attacks have emerged that show that for some of these protocols confidentiality of the data can be compromised, usually given certain auxiliary information. We take a step back and identify a need for a formal understanding of the inherent efficiency/privacy trade-off in outsourced database systems, independent of the details of the system. We propose abstract models that capture secure outsourced storage systems in sufficient generality, and identify two basic sources of leakage, namely access pattern and ommunication volume. We use our models to distinguish certain classes of outsourced database systems that have been proposed, and deduce that all of them exhibit at least one of these leakage sources. We then develop generic reconstruction attacks on any system supporting range queries where either access pattern or communication volume is leaked. These attacks are in a rather weak passive adversarial model, where the untrusted server knows only the underlying query distribution. In particular, to perform our attack the server need not have any prior knowledge about the data, and need not know any of the issued queries nor their results. Yet, the server can reconstruct the secret attribute of every record in the database after about \$Ntextasciicircum4\$ queries, where N is the domain size. We provide a matching lower bound showing that our attacks are essentially optimal. Our reconstruction attacks using communication volume apply even to systems based on homomorphic encryption or oblivious RAM in the natural way. Finally, we provide experimental results demonstrating the efficacy of our attacks on real datasets with a variety of different features. On all these datasets, after the required number of queries our attacks successfully recovered the secret attributes of every record in at most a few seconds.

2017-05-30
Dolev, Shlomi, ElDefrawy, Karim, Lampkins, Joshua, Ostrovsky, Rafail, Yung, Moti.  2016.  Brief Announcement: Proactive Secret Sharing with a Dishonest Majority. Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing. :401–403.

In a secret sharing scheme a dealer shares a secret s among n parties such that an adversary corrupting up to t parties does not learn s, while any t+1 parties can efficiently recover s. Over a long period of time all parties may be corrupted thus violating the threshold, which is accounted for in Proactive Secret Sharing (PSS). PSS schemes periodically rerandomize (refresh) the shares of the secret and invalidate old ones. PSS retains confidentiality even when all parties are corrupted over the lifetime of the secret, but no more than t during a certain window of time, called the refresh period. Existing PSS schemes only guarantee secrecy in the presence of an honest majority with less than n2 total corruptions during a refresh period; an adversary corrupting a single additional party, even if only passively, obtains the secret. This work is the first feasibility result demonstrating PSS tolerating a dishonest majority, it introduces the first PSS scheme secure against t passive adversaries without recovery of lost shares, it can also recover from honest faulty parties losing their shares, and when tolerating e faults the scheme tolerates t passive corruptions. A non-robust version of the scheme can tolerate t active adversaries, and mixed adversaries that control a combination of passively and actively corrupted parties that are a majority, but where less than n/2-e of such corruptions are active. We achieve these high thresholds with O(n4) communication when sharing a single secret, and O(n3) communication when sharing multiple secrets in batches.

Werner, Jan, Baltas, George, Dallara, Rob, Otterness, Nathan, Snow, Kevin Z., Monrose, Fabian, Polychronakis, Michalis.  2016.  No-Execute-After-Read: Preventing Code Disclosure in Commodity Software. Proceedings of the 11th ACM on Asia Conference on Computer and Communications Security. :35–46.

Memory disclosure vulnerabilities enable an adversary to successfully mount arbitrary code execution attacks against applications via so-called just-in-time code reuse attacks, even when those applications are fortified with fine-grained address space layout randomization. This attack paradigm requires the adversary to first read the contents of randomized application code, then construct a code reuse payload using that knowledge. In this paper, we show that the recently proposed Execute-no-Read (XnR) technique fails to prevent just-in-time code reuse attacks. Next, we introduce the design and implementation of a novel memory permission primitive, dubbed No-Execute-After-Read (near), that foregoes the problems of XnR and provides strong security guarantees against just-in-time attacks in commodity binaries. Specifically, near allows all code to be disclosed, but prevents any disclosed code from subsequently being executed, thus thwarting just-in-time code reuse. At the same time, commodity binaries with mixed code and data regions still operate correctly, as legitimate data is still readable. To demonstrate the practicality and portability of our approach we implemented prototypes for both Linux and Android on the ARMv8 architecture, as well as a prototype that protects unmodified Microsoft Windows executables and dynamically linked libraries. In addition, our evaluation on the SPEC2006 benchmark demonstrates that our prototype has negligible runtime overhead, making it suitable for practical deployment.

2017-05-22
Alrwais, Sumayah, Yuan, Kan, Alowaisheq, Eihal, Liao, Xiaojing, Oprea, Alina, Wang, XiaoFeng, Li, Zhou.  2016.  Catching Predators at Watering Holes: Finding and Understanding Strategically Compromised Websites. Proceedings of the 32Nd Annual Conference on Computer Security Applications. :153–166.

Unlike a random, run-of-the-mill website infection, in a strategic web attack, the adversary carefully chooses the target frequently visited by an organization or a group of individuals to compromise, for the purpose of gaining a step closer to the organization or collecting information from the group. This type of attacks, called "watering hole", have been increasingly utilized by APT actors to get into the internal networks of big companies and government agencies or monitor politically oriented groups. With its importance, little has been done so far to understand how the attack works, not to mention any concrete step to counter this threat. In this paper, we report our first step toward better understanding this emerging threat, through systematically discovering and analyzing new watering hole instances and attack campaigns. This was made possible by a carefully designed methodology, which repeatedly monitors a large number potential watering hole targets to detect unusual changes that could be indicative of strategic compromises. Running this system on the HTTP traffic generated from visits to 61K websites for over 5 years, we are able to discover and confirm 17 watering holes and 6 campaigns never reported before. Given so far there are merely 29 watering holes reported by blogs and technical reports, the findings we made contribute to the research on this attack vector, by adding 59% more attack instances and information about how they work to the public knowledge. Analyzing the new watering holes allows us to gain deeper understanding of these attacks, such as repeated compromises of political websites, their long lifetimes, unique evasion strategy (leveraging other compromised sites to serve attack payloads) and new exploit techniques (no malware delivery, web only information gathering). Also, our study brings to light interesting new observations, including the discovery of a recent JSONP attack on an NGO website that has been widely reported and apparently forced the attack to stop.

Hooshmand, Salman, Mahmud, Akib, Bochmann, Gregor V., Faheem, Muhammad, Jourdan, Guy-Vincent, Couturier, Russ, Onut, Iosif-Viorel.  2016.  D-ForenRIA: Distributed Reconstruction of User-Interactions for Rich Internet Applications. Proceedings of the 25th International Conference Companion on World Wide Web. :211–214.

We present D-ForenRIA, a distributed forensic tool to automatically reconstruct user-sessions in Rich Internet Applications (RIAs), using solely the full HTTP traces of the sessions as input. D-ForenRIA recovers automatically each browser state, reconstructs the DOMs and re-creates screenshots of what was displayed to the user. The tool also recovers every action taken by the user on each state, including the user-input data. Our application domain is security forensics, where sometimes months-old sessions must be quickly reconstructed for immediate inspection. We will demonstrate our tool on a series of RIAs, including a vulnerable banking application created by IBM Security for testing purposes. In that case study, the attacker visits the vulnerable web site, and exploits several vulnerabilities (SQL-injections, XSS...) to gain access to private information and to perform unauthorized transactions. D-ForenRIA can reconstruct the session, including screenshots of all pages seen by the hacker, DOM of each page and the steps taken for unauthorized login and the inputs hacker exploited for the SQL-injection attack. D-ForenRIA is made efficient by applying advanced reconstruction techniques and by using several browsers concurrently to speed up the reconstruction process. Although we developed D-ForenRIA in the context of security forensics, the tool can also be useful in other contexts such as aided RIAs debugging and automated RIAs scanning.

Howe, J., Moore, C., O'Neill, M., Regazzoni, F., Güneysu, T., Beeden, K..  2016.  Lattice-based Encryption Over Standard Lattices In Hardware. Proceedings of the 53rd Annual Design Automation Conference. :162:1–162:6.

Lattice-based cryptography has gained credence recently as a replacement for current public-key cryptosystems, due to its quantum-resilience, versatility, and relatively low key sizes. To date, encryption based on the learning with errors (LWE) problem has only been investigated from an ideal lattice standpoint, due to its computation and size efficiencies. However, a thorough investigation of standard lattices in practice has yet to be considered. Standard lattices may be preferred to ideal lattices due to their stronger security assumptions and less restrictive parameter selection process. In this paper, an area-optimised hardware architecture of a standard lattice-based cryptographic scheme is proposed. The design is implemented on a FPGA and it is found that both encryption and decryption fit comfortably on a Spartan-6 FPGA. This is the first hardware architecture for standard lattice-based cryptography reported in the literature to date, and thus is a benchmark for future implementations. Additionally, a revised discrete Gaussian sampler is proposed which is the fastest of its type to date, and also is the first to investigate the cost savings of implementing with λ/2-bits of precision. Performance results are promising compared to the hardware designs of the equivalent ring-LWE scheme, which in addition to providing stronger security proofs; generate 1272 encryptions per second and 4395 decryptions per second.

O'Neill, Maire, O'Sullivan, Elizabeth, McWilliams, Gavin, Saarinen, Markku-Juhani, Moore, Ciara, Khalid, Ayesha, Howe, James, del Pino, Rafael, Abdalla, Michel, Regazzoni, Francesco et al..  2016.  Secure Architectures of Future Emerging Cryptography SAFEcrypto. Proceedings of the ACM International Conference on Computing Frontiers. :315–322.

Funded under the European Union's Horizon 2020 research and innovation programme, SAFEcrypto will provide a new generation of practical, robust and physically secure post-quantum cryptographic solutions that ensure long-term security for future ICT systems, services and applications. The project will focus on the remarkably versatile field of Lattice-based cryptography as the source of computational hardness, and will deliver optimised public key security primitives for digital signatures and authentication, as well identity based encryption (IBE) and attribute based encryption (ABE). This will involve algorithmic and design optimisations, and implementations of lattice-based cryptographic schemes addressing cost, energy consumption, performance and physical robustness. As the National Institute of Standards and Technology (NIST) prepares for the transition to a post-quantum cryptographic suite B, urging organisations that build systems and infrastructures that require long-term security to consider this transition in architectural designs; the SAFEcrypto project will provide Proof-of-concept demonstrators of schemes for three practical real-world case studies with long-term security requirements, in the application areas of satellite communications, network security and cloud. The goal is to affirm Lattice-based cryptography as an effective replacement for traditional number-theoretic public-key cryptography, by demonstrating that it can address the needs of resource-constrained embedded applications, such as mobile and battery-operated devices, and of real-time high performance applications for cloud and network management infrastructures.

Keller, Marcel, Orsini, Emmanuela, Scholl, Peter.  2016.  MASCOT: Faster Malicious Arithmetic Secure Computation with Oblivious Transfer. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :830–842.

We consider the task of secure multi-party computation of arithmetic circuits over a finite field. Unlike Boolean circuits, arithmetic circuits allow natural computations on integers to be expressed easily and efficiently. In the strongest setting of malicious security with a dishonest majority –- where any number of parties may deviate arbitrarily from the protocol –- most existing protocols require expensive public-key cryptography for each multiplication in the preprocessing stage of the protocol, which leads to a high total cost. We present a new protocol that overcomes this limitation by using oblivious transfer to perform secure multiplications in general finite fields with reduced communication and computation. Our protocol is based on an arithmetic view of oblivious transfer, with careful consistency checks and other techniques to obtain malicious security at a cost of less than 6 times that of semi-honest security. We describe a highly optimized implementation together with experimental results for up to five parties. By making extensive use of parallelism and SSE instructions, we improve upon previous runtimes for MPC over arithmetic circuits by more than 200 times.

O'Brien, Heather L., Freund, Luanne, Kopak, Richard.  2016.  Investigating the Role of User Engagement in Digital Reading Environments. Proceedings of the 2016 ACM on Conference on Human Information Interaction and Retrieval. :71–80.

User engagement is recognized as an important component of the user experience, but relatively little is known about the effect of engagement on the learning outcomes of such interactions. This experimental user study examines the relationship between user engagement (UE) and comprehension in varied academic reading environments. Forty-one university students interacted with one of two sets of texts presented in 4 conditions in the context of preparing for a class assignment. Employing the User Engagement Scale (UES), we found evidence of a relationship between students' comprehension of the texts and their degree of engagement with them. However, this association was confined to one of the UES subscales and was not consistent across levels of engagement. An examination of additional variables found little evidence that system and content characteristics influenced engagement; however, we noted that all students' reported increased knowledge, but topical interest for non-engaged students declined. Results contribute to existing literature by adding further evidence that the relationship between engagement and comprehension is complex and mediated.

2017-05-18
Saurez, Enrique, Hong, Kirak, Lillethun, Dave, Ramachandran, Umakishore, Ottenwälder, Beate.  2016.  Incremental Deployment and Migration of Geo-distributed Situation Awareness Applications in the Fog. Proceedings of the 10th ACM International Conference on Distributed and Event-based Systems. :258–269.

Geo-distributed Situation Awareness applications are large in scale and are characterized by 24/7 data generation from mobile and stationary sensors (such as cameras and GPS devices); latency-sensitivity for converting sensed data to actionable knowledge; and elastic and bursty needs for computational resources. Fog computing [7] envisions providing computational resources close to the edge of the network, consequently reducing the latency for the sense-process-actuate cycle that exists in these applications. We propose Foglets, a programming infrastructure for the geo-distributed computational continuum represented by fog nodes and the cloud. Foglets provides APIs for a spatio-temporal data abstraction for storing and retrieving application generated data on the local nodes, and primitives for communication among the resources in the computational continuum. Foglets manages the application components on the Fog nodes. Algorithms are presented for launching application components and handling the migration of these components between Fog nodes, based on the mobility pattern of the sensors and the dynamic computational needs of the application. Evaluation results are presented for a Fog network consisting of 16 nodes using a simulated vehicular network as the workload. We show that the discovery and deployment protocol can be executed in 0.93 secs, and joining an already deployed application can be as quick as 65 ms. Also, QoS-sensitive proactive migration can be accomplished in 6 ms.

Fedosov, Anton, Ojala, Jarno, Niforatos, Evangelos, Olsson, Thomas, Langheinrich, Marc.  2016.  Mobile First?: Understanding Device Usage Practices in Novel Content Sharing Services Proceedings of the 20th International Academic Mindtrek Conference. :198–207.

Today's mobile app economy has greatly expanded the types of "things" people can share –- spanning from new types of digital content like physiological data (e.g., workouts) to physical things like apartments and work tools ("sharing economy"). To understand whether mobile platforms provide adequate support for such novel sharing services, we surveyed 200 participants about their experiences with six types of emergent sharing services. For each domain we elicited device usage practices and identified corresponding device selection criteria. Our analysis suggests that, despite contemporary mobile first design efforts, desktop interfaces of emergent content sharing services are often considered more efficient and easier to use –- both for sharing and access control tasks (i.e., privacy). Based on our findings, we outline device-related design and research opportunities in this space.

2017-05-17
Bae, Kyungmin, Ölveczky, Peter Csaba, Kong, Soonho, Gao, Sicun, Clarke, Edmund M..  2016.  SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems. Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. :145–154.

This paper presents general techniques for verifying virtually synchronous distributed control systems with interconnected physical environments. Such cyber-physical systems (CPSs) are notoriously hard to verify, due to their combination of nontrivial continuous dynamics, network delays, imprecise local clocks, asynchronous communication, etc. To simplify their analysis, we first extend the PALS methodology–-that allows to abstract from the timing of events, asynchronous communication, network delays, and imprecise clocks, as long as the infrastructure guarantees bounds on the network delays and clock skews–-from real-time to hybrid systems. We prove a bisimulation equivalence between Hybrid PALS synchronous and asynchronous models. We then show how various verification problems for synchronous Hybrid PALS models can be reduced to SMT solving over nonlinear theories of the real numbers. We illustrate the Hybrid PALS modeling and verification methodology on a number of CPSs, including a control system for turning an airplane.

Ouaknine, Joel, Pouly, Amaury, Sousa-Pinto, Joao, Worrell, James.  2016.  Solvability of Matrix-Exponential Equations. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. :798–806.

We consider a continuous analogue of (Babai et al. 1996)'s and (Cai et al. 2000)'s problem of solving multiplicative matrix equations. Given k + 1 square matrices A1, ..., Ak, C, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals t1, ..., tk such that We show that this problem is undecidable in general, but decidable under the assumption that the matrices A1, ..., Ak commute. Our results have applications to reachability problems for linear hybrid automata. Our decidability proof relies on a number of theorems from algebraic and transcendental number theory, most notably those of Baker, Kronecker, Lindemann, and Masser, as well as some useful geometric and linear-algebraic results, including the Minkowski-Weyl theorem and a new (to the best of our knowledge) result about the uniqueness of strictly upper triangular matrix logarithms of upper unitriangular matrices. On the other hand, our undecidability result is shown by reduction from Hilbert's Tenth Problem.

Oluwatimi, Oyindamola, Midi, Daniele, Bertino, Elisa.  2016.  A Context-Aware System to Secure Enterprise Content. Proceedings of the 21st ACM on Symposium on Access Control Models and Technologies. :63–72.

In this paper, we present an architecture and implementation of a secure, automated, proximity-based access control that we refer to as Context-Aware System to Secure Enterprise Content (CASSEC). Using the pervasive WiFi and Bluetooth wireless devices as components in our underlying positioning infrastructure, CASSEC addresses two proximity-based scenarios often encountered in enterprise environments: Separation of Duty and Absence of Other Users. The first scenario is achieved by using Bluetooth MAC addresses of nearby occupants as authentication tokens. The second scenario exploits the interference of WiFi received signal strength when an occupant crosses the line of sight (LOS). Regardless of the scenario, information about the occupancy of a particular location is periodically extracted to support continuous authentication. To the best of our knowledge, our approach is the first to incorporate WiFi signal interference caused by occupants as part of proximity-based access control system. Our results demonstrate that it is feasible to achieve great accuracy in localization of occupants in a monitored room.

Ostberg, Jan-Peter, Wagner, Stefan, Weilemann, Erica.  2016.  Does Personality Influence the Usage of Static Analysis Tools?: An Explorative Experiment Proceedings of the 9th International Workshop on Cooperative and Human Aspects of Software Engineering. :75–81.

There are many techniques to improve software quality. One is using automatic static analysis tools. We have observed, however, that despite the low-cost help they offer, these tools are underused and often discourage beginners. There is evidence that personality traits influence the perceived usability of a software. Thus, to support beginners better, we need to understand how the workflow of people with different prevalent personality traits using these tools varies. For this purpose, we observed users' solution strategies and correlated them with their prevalent personality traits in an exploratory study with student participants within a controlled experiment. We gathered data by screen capturing and chat protocols as well as a Big Five personality traits test. We found strong correlations between particular personality traits and different strategies of removing the findings of static code analysis as well as between personality and tool utilization. Based on that, we offer take-away improvement suggestions. Our results imply that developers should be aware of these solution strategies and use this information to build tools that are more appealing to people with different prevalent personality traits.

2017-05-16
Fiore, Dario, Fournet, Cédric, Ghosh, Esha, Kohlweiss, Markulf, Ohrimenko, Olga, Parno, Bryan.  2016.  Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :1304–1316.

Proof systems for verifiable computation (VC) have the potential to make cloud outsourcing more trustworthy. Recent schemes enable a verifier with limited resources to delegate large computations and verify their outcome based on succinct arguments: verification complexity is linear in the size of the inputs and outputs (not the size of the computation). However, cloud computing also often involves large amounts of data, which may exceed the local storage and I/O capabilities of the verifier, and thus limit the use of VC. In this paper, we investigate multi-relation hash & prove schemes for verifiable computations that operate on succinct data hashes. Hence, the verifier delegates both storage and computation to an untrusted worker. She uploads data and keeps hashes; exchanges hashes with other parties; verifies arguments that consume and produce hashes; and selectively downloads the actual data she needs to access. Existing instantiations that fit our definition either target restricted classes of computations or employ relatively inefficient techniques. Instead, we propose efficient constructions that lift classes of existing arguments schemes for fixed relations to multi-relation hash & prove schemes. Our schemes (1) rely on hash algorithms that run linearly in the size of the input; (2) enable constant-time verification of arguments on hashed inputs; (3) incur minimal overhead for the prover. Their main benefit is to amortize the linear cost for the verifier across all relations with shared I/O. Concretely, compared to solutions that can be obtained from prior work, our new hash & prove constructions yield a 1,400x speed-up for provers. We also explain how to further reduce the linear verification costs by partially outsourcing the hash computation itself, obtaining a 480x speed-up when applied to existing VC schemes, even on single-relation executions.

Oswald, David F..  2016.  Wireless Attacks on Automotive Remote Keyless Entry Systems. Proceedings of the 6th International Workshop on Trustworthy Embedded Devices. :43–44.

Modern vehicles rely on a variety of electronic systems and components. One of those components is the vehicle key. Today, a key typically implements at least three functions: mechanical locking with a key blade, the electronic immobilizer to autorise the start of the engine, and the remote keyless entry (RKE) system that allows to wirelessly (un)lock the doors and disable the alarm system. These main components of a vehicle key are shown in Figure 1. For the mechanical part of the vehicle key, it is well known that the key blade can be easily copied and that the locking cylinder can be bypassed with other means (using so-called "decoders" or simply a screwdriver). In contrast, immobilizer and RKE rely on wireless protocols to cryptographically authenticate the vehicle key to the car. Immobilizers employ radio frequency identification (RFID) transponders to carry out a challenge-response protocol over a low-range bidirectional link at a frequency of 125 kHz. In the past, researchers have revealed severe aws in the cryptography and protocols used by immobilizers, leading to the break of the major systems Megamos, Hitag2, and DST40 [7, 6, 1]. In contrast to the immobilizer, the RKE part uses unidirectional communication (the vehicle only receives, the key fob only transmits) over a high-range wireless link with operating distances of tens to one hundred meters. These systems are based on rolling codes, which essentially transmit a counter (that is incremented on each button press) in a cryptographically authenticated manner. Until recently, the security of automotive RKE had been scrutinized to a lesser degree than that of immobilizers, even though vulnerabilities in similar systems have been known since 2008 with the attacks on KeeLoq [3]. Other results reported in the literature include an analytical attack on a single, outdated vehicle [2] and the so-called "RollJam" technique [5], which is based on a combination of replay and selective jamming. In 2016, it was shown that severe aws exist in the RKE systems of major automotive manufacturers [4]. On the one hand, the VWgroup (Volkswagen, Seat, Skoda, Audi) based the security of their RKE system on a few global cryptographic keys, potentially affecting hundreds of million vehicles world-wide. By extracting these global keys from the firmware of electronic controls units (ECUs) once, an adversary is able to create a duplicate of the owner's RKE fob by eavesdropping a single rolling code. The second case study in [4] exposes new cryptographic weaknesses in the Hitag2 cipher when used for RKE. Applying a correlation-based attack, an adversary can recover the 48-bit cryptographic key by eavesdropping four to eight rolling codes and performing a one-minute computation on a standard laptop. Again, this attack affects millions of vehicle world-wide. Manufacturers that used Hitag2 in their RKE system include Alfa Romeo, Peugeot, Lancia, Opel, Renault, and Ford among others. In this keynote talk, we will present the results of [4] and put them in into a broader context by revisiting the history of attacks on RKE systems and automotive electronics.