Biblio

In this research paper, we describe an algorithm that could be implemented on an intrusion response system (IRS) designed specifically for mobile ad hoc networks (MANET). Designed to supplement a MANET's hierarchical intrusion detection system (IDS), this IRS and its associated algorithm would be implemented on the root node operating in such an IRS, and would rely on the optimized link state routing protocol (OLSR) to determine facts about the topology of the network, and use that determination to facilitate responding to network intrusions and attacks. The algorithm operates in a query-response mode, where the IRS function of the IDS root node queries the implemented algorithm, and the algorithm returns its response, formatted as an unordered list of nodes satisfying the query.

An anonymous identification scheme for ad hoc group allows a participant to identify himself as a member of a group of users in a way that his actual identity is not revealed. We propose a highly efficient construction of this cryptographic primitive in the symmetric key setting based on the idea of program obfuscation. The salient feature of our scheme is that only hash evaluations are needed. Consequently, our scheme outperforms all existing constructions for a reasonably large ad hoc group size (of around 50000 users) since no exponentiation nor pairing operation is involved. Technically, the participant only needs to evaluate one hash operation to identify himself. While the time complexity of the verifier is linearly in the size of the ad hoc group, the actual running time is rather insignificant since the constant factor of this linear dependence is the time of a single hash evaluation. To analyse the security of our proposal, we develop a security model to capture the security requirements of this primitive and prove that our construction satisfies these requirements in the random oracle model against unbounded attackers. Similar to other identification schemes secure in the random oracle model, our proposed protocol requires only two message flow.

Technology coined as the vehicular ad hoc network (VANET) is harmonizing with Intelligent Transportation System (ITS) and Intelligent Traffic System (ITF). An application scenario of VANET is the military communication where vehicles move as a convoy on roadways, requiring secure and reliable communication. However, utilization of radio frequency (RF) communication in VANET limits its usage in military applications, due to the scarce frequency band and its vulnerability to security attacks. Visible Light Communication (VLC) has been recently introduced as a more secure alternative, limiting the reception of neighboring nodes with its directional transmission. However, secure vehicular VLC that ensures confidential data transfer among the participating vehicles, is an open problem. In this paper, we propose a secure military light communication protocol (SecVLC) for enabling efficient and secure data sharing. We use the directionality property of VLC to ensure that only target vehicles participate in the communication. Vehicles use full-duplex communication where infra-red (IR) is utilized to share a secret key and VLC is used to receive encrypted data. We experimentally demonstrate the suitability of SecVLC in outdoor scenarios at varying inter-vehicular distances with key metrics of interest, including the security, data packet delivery ratio and delay.

This demo shows how two objects that each live within their own world, i.e., the are not in each others transitive closure of object references, can get to know each other in a well-defined manner using a new language construct. The basic problem is that if two object are in different worlds, there is no way they can communicate. Our proposed language construct, added to the Emerald programming language, allows objects in close proximity to get to know each other in a well-defined, language based manner.

In this paper, we present a novel acoustic sensing technique that recognizes two convenient input actions: hand gestures and on-body touch. We achieved them by observing the frequency spectrum of the wave propagated in the body, around the periphery of the wrist. Our approach can recognize hand gestures and on-body touch concurrently in real-time and is expected to obtain rich input variations by combining them. We conducted a user study that showed classification accuracy of 97%, 96%, and 97% for hand gestures, touches on the forearm, and touches on the back of the hand.

Over the last decade, differential privacy has achieved widespread adoption within the privacy community. Moreover, it has attracted significant attention from the verification community, resulting in several successful tools for formally proving differential privacy. Although their technical approaches vary greatly, all existing tools rely on reasoning principles derived from the composition theorem of differential privacy. While this suffices to verify most common private algorithms, there are several important algorithms whose privacy analysis does not rely solely on the composition theorem. Their proofs are significantly more complex, and are currently beyond the reach of verification tools. In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based on deep connections between differential privacy and probabilistic couplings, an established mathematical tool for reasoning about stochastic processes. Even when the composition theorem is not helpful, we can often prove privacy by a coupling argument. We demonstrate our methods on two algorithms: the Exponential mechanism and the Above Threshold algorithm, the critical component of the famous Sparse Vector algorithm. We verify these examples in a relational program logic apRHL+, which can construct approximate couplings. This logic extends the existing apRHL logic with more general rules for the Laplace mechanism and the one-sided Laplace mechanism, and new structural rules enabling pointwise reasoning about privacy; all the rules are inspired by the connection with coupling. While our paper is presented from a formal verification perspective, we believe that its main insight is of independent interest for the differential privacy community.

Existing anti-debugging protections are relatively weak. In existing self-debugger approaches, a custom debugger is attached to the main application, of which the control flow is obfuscated by redirecting it through the debugger. The coupling between the debugger and the main application is then quite loose, and not that hard to break by an attacker. In the tightly-coupled self-debugging technique proposed in this paper, full code fragments are migrated from the application to the debugger, making it harder for the attacker to reverse-engineer the program and to deconstruct it into the original unprotected program to attach a debugger or to collect traces. We evaluate a prototype implementation on three complex, real-world Android use cases and present the results of tests conducted by professional penetration testers.

This paper presents DopEnc, an acoustic-based encounter profiling system on smartphones. DopEnc can automatically identify the persons that users interact with in the context of encountering. DopEnc performs encounter profiling in two major steps: (1) Doppler profiling to detect that two persons approach and stop in front of each other via an effective trajectory, and (2) voice profiling to confirm that they are thereafter engaged in an interactive conversation. DopEnc is further extended to support parallel acoustic exploration of many users by incorporating a unique multiple access scheme within the limited inaudible acoustic frequency band. All implementation of DopEnc is based on commodity sensors like speakers, microphones and accelerometers integrated on commercial-off-the-shelf smartphones. We evaluate DopEnc with detailed experiments and a real use-case study of 11 participants. Overall DopEnc achieves an accuracy of 6.9% false positive and 9.7% false negative in real usage.

This paper presents a simulator for swarm operations designed to verify algorithms for a swarm of autonomous underwater robots (AUVs), specifically for constructing an underwater communication network with AUVs carrying acoustic communication devices. This simulator consists of three nodes: a virtual vehicle node (VV), a virtual environment node (VE), and a visual showing node (VS). The modular design treats AUV models as a combination of virtual equipment. An expert acoustic communication simulator is embedded in this simulator, to simulate scenarios with dynamic acoustic communication nodes. The several simulations we have performed demonstrate that this simulator is easy to use and can be further improved.

Collaborative information seeking frequently occurs in an opportunistic and loosely-coupled fashion that is supported by awareness of others' activities on the web. Automatically sharing traces of information about web activity could substantially improve these collaborative information tasks, but conventional wisdom suggests that people are very reluctant to share information about web usage. Because work settings have different rules and practices about privacy, we carried out the first systematic study of people's privacy concerns about sharing web activity within workgroups. To provide a better understanding of privacy concerns about sharing web activity at work, we conducted a two-week diary study with 18 participants. Our study system asked participants to report on their search tasks and privacy concerns. Surprisingly, our results showed that people have little concern about sharing the majority of their activities with their work colleagues, and had even fewer concerns with sharing work-related activities. Our results provide new insights into the possibilities of sharing web activities within workgroups, and provide evidence that tools based on automatic sharing of awareness information can be feasible.

This paper aims at building a sparse deep autoencoder network with joint regularizations for image super-resolution. A map is learned from the low-resolution feature space to high-resolution feature space. In the training stage, two autoencoder networks are built for image representation for low resolution images and their high resolution counterparts, respectively. A neural network is constructed to learn a map between the features of low resolution images and high resolution images. Furthermore, due to the local smoothness and the redundancy of an image, the joint variation regularizations are unified with the coupled autoencoder network (CAN). For the local smoothness, steerable kernel variation regularization is designed. For redundancy, non-local variation regularization is designed. The joint regularizations improve the quality of the super resolution image. Experimental results on Set5 demonstrate the effectiveness of our proposed method.

In this paper we explore how to embed status information of IoT-enabled devices in the acoustic atmosphere using melodic ambient sounds while limiting obtrusiveness for the user. The user can use arbitrary sound samples to represent the devices he wants to monitor. Our system combines these sound samples into a melodic ambient rhythm that contains information on all the processes or variables that user is monitoring. We focus on continuous rather than binary information (e.g. "monitoring progress status" rather then "new message received"). We evaluate our system in a machine monitoring scenario focusing on 5 distinct machines/processes to monitor with 6 priority levels for each. 9 participants use our system to monitor these processes with an up to 92.44% detection rate, if several levels are combined. Participants had no previous experience with this or similar systems and had only 5-10 minute training session before the tests.

We consider 3-dimensional(3D) underwater random network (UAN) where the nodes are uniformly distributed in a cuboid region. Then we derive the closed-form probability of finding a receiver in an ellipsoid neighborhood of an arbitrary sender. Computer simulation shows that the analytical result is generally consistent with the simulated result.

More and more current industrial control systems (e.g, smart grids, oil and gas systems, connected cars and trucks) have the capability to collect and transmit users' data in order to provide services that are tailored to the specific needs of the customers. Such smart industrial control systems fall into the category of Internet of Things (IoT). However, in many cases, the data transmitted by such IoT devices includes sensitive information and users are faced with an all-or-nothing choice: either they adopt the proposed services and release their private data, or refrain from using services which could be beneficial but pose significant privacy risks. Unfortunately, encryption alone does not solve the problem, though techniques to counter these privacy risks are emerging (e.g., by using applications that alter, merge or bundle data to ensure they cannot be linked to a particular user). In this paper, we propose a general framework, whereby users can not only specify how their data is managed, but also restrict data collection from their connected devices. More precisely, we propose to use data collection policies to govern the transmission of data from IoT devices, coupled with policies to ensure that once the data has been transmitted, it is stored and shared in a secure way. To achieve this goal, we have designed a framework for secure data collection, storage and management, with logical foundations that enable verification of policy properties.

Emerging technologies such as the Internet of Things (IoT) heavily rely on hardware security for data and privacy protection. However, constantly increasing integration complexity requires automatic synthesis to maintain the pace of innovation. We introduce the first High-Level Synthesis (HLS) flow that produces a security enhanced hardware design to directly prevent Hardware Trojan Horse (HTH) injection by a malicious foundry. Through analysis of entropy loss and criticality decay, the presented algorithms implement highly efficient resource-targeted information dispersion to counter HTH insertion. The flow is evaluated on existing HLS benchmarks and a new IoT-specific benchmark and shows significant resource savings.

Access Control Policies are used to specify who can access which resource under which conditions, and ensuring their correctness is vital to prevent security breaches. As access control policies can be complex and error-prone, we propose an original framework that supports the validation of the implemented policies (specified in the standard XACML notation) against the intended rights, which can be informally expressed, e.g. in tabular form. The framework relies on well-known software testing technology, such as mutation and combinatorial techniques. The paper presents the implemented environment and an application example.

Administration of access control policies is a difficult task, especially in large organizations. We consider the problem of detecting whether administrative actions can yield in policies where some security goals are compromised. In particular, we are interested in problems generated by modifications –- such as adding/deleting elements to/from the set of possible users or permissions –- of policies specified as term-rewrite systems. We propose to use rewriting techniques to compare the behaviors of the modified version and the original version of the policy. More precisely, we use narrowing to compute counter-examples to the equivalence of rewrite-based policies. We prove that our technique provides a sound and complete way to recursively enumerate the set of counter-examples, even when this set is not finite, or when a mistake of the administrator makes one or both systems non-terminating.

We describe the formalization of a correctness proof for a conflict detection algorithm for XACML (eXtensible Access Control Markup Language). XACML is a standardized declarative access control policy language that is increasingly used in industry. In practice it is common for rule sets to grow large, and contain unintended errors, often due to conflicting rules. A conflict occurs in a policy when one rule permits a request and another denies that same request. Such errors can lead to serious risks involving both allowing access to an unauthorized user as well as denying access to someone who needs it. Removing conflicts is thus an important aspect of debugging policies, and the use of a verified algorithm provides the highest assurance in a domain where security is important. In this paper, we focus on several complex XACML constructs, including time ranges and integer intervals, as well as ways to combine any number of functions using the boolean operators and, or, and not. The latter are the most complex, and add significant expressive power to the language. We propose an algorithm to find conflicts and then use the Coq Proof Assistant to prove the algorithm correct. We develop a library of tactics to help automate the proof.

In this paper we describe a system that allows the real time creation of firewall rules in response to geographic and political changes in the control-plane. This allows an organization to mitigate data exfiltration threats by analyzing Border Gateway Protocol (BGP) updates and blocking packets from being routed through problematic jurisdictions. By inspecting the autonomous system paths and referencing external data sources about the autonomous systems, a BGP participant can infer the countries that traffic to a particular destination address will traverse. Based on this information, an organization can then define constraints on its egress traffic to prevent sensitive data from being sent via an untrusted region. In light of the many route leaks and BGP hijacks that occur today, this offers a new option to organizations willing to accept reduced availability over the risk to confidentiality. Similar to firewalls that allow organizations to block traffic originating from specific countries, our approach allows blocking outbound traffic from transiting specific jurisdictions. To illustrate the efficacy of this approach, we provide an analysis of paths to various financial services IP addresses over the course of a month from a single BGP vantage point that quantifies the frequency of path alterations resulting in the traversal of new countries. We conclude with an argument for the utility of country-based egress policies that do not require the cooperation of upstream providers.

Security mechanism of the mobile agent running platform is very important for mobile agent system operation and stability running. In this paper we mainly focus on the security issues related with the mobile agent running platform and we proposed a cross validation mechanism mixed with encryption algorithm to solve the security problems during the migration and communication of mobile agents. Firstly, we employ the cross-validation mechanism to authenticate the nodes mobile agents will be visiting. Secondly, we employ the hybrid encryption mechanism, which combines the advantages of the symmetric encryption and asymmetric encryption, to encrypt the mobile agents and ensure the transferring process of data. Finally, we employ the EMSSL socket communication method to encrypt the content of transmission, in turn to enhance the security and robustness of the mobile agent system. We implement several experiments in the simulation environment and the experimental results verify the efficiency and accuracy of the proposed methods.

Network architectures and applications are becoming increasingly complex. Several approaches to automatically enforce configurations on devices, applications and services have been proposed, such as Policy-Based Network Management (PBNM). However, the management of enforced configurations in production environments (e.g. data center) is a crucial and complex task. For example, updates on firewall configuration to change a set of rules. Although this task is fundamental for complex systems, few effective solutions have been proposed for monitoring and managing enforced configurations. This work proposes a novel approach to monitor and manage enforced configurations in production environments. The main contributions of this paper are a formal model to identify/ generate traffic flows and to verify the enforced configurations; and a slim and transparent framework to perform the policy assessment. We have implemented and validated our approach in a virtual environment in order to evaluate different scenarios. The results demonstrate that the prototype is effective and has good performance, therefore our model can be effectively used to analyse several types of IT infrastructures. A further interesting result is that our approach is complementary to PBNM.

The popularity of cloud hosting services also brings in new security challenges: it has been reported that these services are increasingly utilized by miscreants for their malicious online activities. Mitigating this emerging threat, posed by such "bad repositories" (simply Bar), is challenging due to the different hosting strategy to traditional hosting service, the lack of direct observations of the repositories by those outside the cloud, the reluctance of the cloud provider to scan its customers' repositories without their consent, and the unique evasion strategies employed by the adversary. In this paper, we took the first step toward understanding and detecting this emerging threat. Using a small set of "seeds" (i.e., confirmed Bars), we identified a set of collective features from the websites they serve (e.g., attempts to hide Bars), which uniquely characterize the Bars. These features were utilized to build a scanner that detected over 600 Bars on leading cloud platforms like Amazon, Google, and 150K sites, including popular ones like groupon.com, using them. Highlights of our study include the pivotal roles played by these repositories on malicious infrastructures and other important discoveries include how the adversary exploited legitimate cloud repositories and why the adversary uses Bars in the first place that has never been reported. These findings bring such malicious services to the spotlight and contribute to a better understanding and ultimately eliminating this new threat.

The automotive industry is experiencing a paradigm shift towards autonomous and connected vehicles. Coupled with the increasing usage and complexity of electrical and/or electronic systems, this introduces new safety and security risks. Encouragingly, the automotive industry has relatively well-known and standardised safety risk management practices, but security risk management is still in its infancy. In order to facilitate the derivation of security requirements and security measures for automotive embedded systems, we propose a specifically tailored risk assessment framework, and we demonstrate its viability with an industry use-case. Some of the key features are alignment with existing processes for functional safety, and usability for non-security specialists. The framework begins with a threat analysis to identify the assets, and threats to those assets. The following risk assessment process consists of an estimation of the threat level and of the impact level. This step utilises several existing standards and methodologies, with changes where necessary. Finally, a security level is estimated which is used to formulate high-level security requirements. The strong alignment with existing standards and processes should make this framework well-suited for the needs in the automotive industry.

The computer security community has long advocated defense in depth, building multiple layers of defense to protect a system. Realizing this vision is not yet practical, as software often ships with inadequate defenses, typically developed in an ad hoc fashion. Currently, programmers reason about security manually and lack tools to validate assurance that security controls provide satisfactory defenses. In this keynote talk, I will discuss how achieving defense in depth has a significant component in configuration. In particular, we advocate configuring security requirements for various layers of software defenses (e.g., privilege separation, authorization, and auditing) and generating software and systems defenses that implement such configurations (mostly) automatically. I will focus mainly on the challenge of retrofitting software with authorization code automatically to demonstrate the configuration problems faced by the community, and discuss how we may leverage these lessons to configuring software and systems for defense in depth.

Firewall policies are notorious for having misconfiguration errors which can defeat its intended purpose of protecting hosts in the network from malicious users. We believe this is because today's firewall policies are mostly monolithic. Inspired by ideas from modular programming and code refactoring, in this work we introduce three kinds of modules: primary, auxiliary, and template, which facilitate the refactoring of a firewall policy into smaller, reusable, comprehensible, and more manageable components. We present algorithms for generating each of the three modules for a given legacy firewall policy. We also develop ModFP, an automated tool for converting legacy firewall policies represented in access control list to their modularized format. With the help of ModFP, when examining several real-world policies with sizes ranging from dozens to hundreds of rules, we were able to identify subtle errors.