Biblio

Protecting data confidentiality and integrity has become increasingly important in modern software. Sometimes, access control mechanisms come short and solutions on the application-level are needed. An approach can rely on enforcing information security using some features provided by certain programming languages. Several different solutions addressing this problem have been presented in literature, and entire new languages or libraries have been built from scratch. Some of them use type systems to let the compiler check for vulnerable code. In this way we are able to rule out those implementations which do not meet a certain security requirement. In this paper we use Haskell's type system to enforce three key properties of information security: non-interference and flexible declassification policies, strict input validation, and secure computations on untainted and trusted values. We present a functional lightweight library for applications with data integrity and confidentiality issues. Our contribute relies on a compile time enforcing of the aforementioned properties. Our library is wholly generalized and might be adapted for satisfying almost every security requirement.

We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.

Searchable encryption (SE) allows a client to outsource a dataset to an untrusted server while enabling the server to answer keyword queries in a private manner. SE can be used as a building block to support more expressive private queries such as range/point and boolean queries, while providing formal security guarantees. To scale SE to big data using external memory, new schemes with small locality have been proposed, where locality is defined as the number of non-continuous reads that the server makes for each query. Previous space-efficient SE schemes achieve optimal locality by increasing the read efficiency-the number of additional memory locations (false positives) that the server reads per result item. This can hurt practical performance. In this work, we design, formally prove secure, and evaluate the first SE scheme with tunable locality and linear space. Our first scheme has optimal locality and outperforms existing approaches (that have a slightly different leakage profile) by up to 2.5 orders of magnitude in terms of read efficiency, for all practical database sizes. Another version of our construction with the same leakage as previous works can be tuned to have bounded locality, optimal read efficiency and up to 60x more efficient end-to-end search time. We demonstrate that our schemes work fast in in-memory as well, leading to search time savings of up to 1 order of magnitude when compared to the most practical in-memory SE schemes. Finally, our construction can be tuned to achieve trade-offs between space, read efficiency, locality, parallelism and communication overhead.

Validating security properties of complex distributed systems is a challenging problem by itself, let alone when the work needs to be performed under tight budget and time constraints on prototype systems with components at various maturity levels. This paper described a tailored approach to security evaluations involving a strategic combination of model-based quantification, emulation, and logical argumentation. By customizing the evaluation to fit existing budget and timelines, validators can achieve the most appropriate validation process, trading off fidelity with coverage across a number of different defense components and different maturity levels. We successfully applied this process to the validation of an overlay proxy network, analyzing the impact of five different defense attributes (together with combinations thereof) on access path establishment and anonymity.

In this paper, we describe an abstraction-based method for synthesizing a state-based switching control for stabilizing a family of dynamical systems. Given a set of dynamical systems and a set of polyhedral switching surfaces, the algorithm synthesizes a strategy that assigns to every surface the linear dynamics to switch to at the surface. Our algorithm constructs a finite game graph that consists of the switching surfaces as the existential nodes and the choices of the dynamics as the universal nodes. In addition, the edges capture quantitative information about the evolution of the distance of the state from the equilibrium point along the executions. A switching strategy for the family of dynamical systems is extracted by finding a strategy on the game graph which results in plays having a bounded weight. Such a strategy is obtained by reducing the problem to the strategy synthesis for an energy game, which is a well-studied problem in the literature. We have implemented our algorithm for polyhedral inclusion dynamics and linear dynamics. We illustrate our algorithm on examples from these two classes of systems.

Nakamoto's famous blockchain protocol enables achieving consensus in a so-called permissionless setting—anyone can join (or leave) the protocol execution, and the protocol instructions do not depend on the identities of the players. His ingenious protocol prevents "sybil attacks" (where an adversary spawns any number of new players) by relying on computational puzzles (a.k.a. "moderately hard functions") introduced by Dwork and Naor (Crypto'92). Recent work by Garay et al (EuroCrypt'15) and Pass et al (manuscript, 2016) demonstrate that this protocol provably achieves consistency and liveness assuming a) honest players control a majority of the computational power in the network, b) the puzzle-hardness is appropriately set as a function of the maximum network delay and the total computational power of the network, and c) the computational puzzle is modeled as a random oracle. Assuming honest participation, however, is a strong assumption, especially in a setting where honest players are expected to perform a lot of work (to solve the computational puzzles). In Nakamoto's Bitcoin application of the blockchain protocol, players are incentivized to solve these puzzles by receiving rewards for every "block" (of transactions) they contribute to the blockchain. An elegant work by Eyal and Sirer (FinancialCrypt'14), strengthening and formalizing an earlier attack discussed on the Bitcoin forum, demonstrates that a coalition controlling even a minority fraction of the computational power in the network can gain (close to) 2 times its "fair share" of the rewards (and transaction fees) by deviating from the protocol instructions. In contrast, in a fair protocol, one would expect that players controlling a φ fraction of the computational resources to reap a φ fraction of the rewards. We present a new blockchain protocol—the FruitChain protocol—which satisfies the same consistency and liveness properties as Nakamoto's protocol (assuming an honest majority of the computing power), and additionally is δ-approximately fair: with overwhelming probability, any honest set of players controlling a φ fraction of computational power is guaranteed to get at least a fraction (1-δ)φ of the blocks (and thus rewards) in any Ω(κ/δ) length segment of the chain (where κ is the security parameter). Consequently, if this blockchain protocol is used as the ledger underlying a cryptocurrency system, where rewards and transaction fees are evenly distributed among the miners of blocks in a length κ segment of the chain, no coalition controlling less than a majority of the computing power can gain more than a factor (1+3δ) by deviating from the protocol (i.e., honest participation is an n/2-coalition-safe 3δ-Nash equilibrium). Finally, the FruitChain protocol enables decreasing the variance of mining rewards and as such significantly lessens (or even obliterates) the need for mining pools.

Motivated by the need to automatically generate behavior-based security challenges to improve user authentication for web services, we consider the problem of large-scale construction of realistic-looking names to serve as aliases for real individuals. We aim to use these names to construct security challenges, where users are asked to identify their real contacts among a presented pool of names. We seek these look-alike names to preserve name characteristics like gender, ethnicity, and popularity, while being unlinkable back to the source individual, thereby making the real contacts not easily guessable by attackers. To achive this, we introduce the technique of distributed name embeddings, representing names in a high-dimensional space such that distance between name components reflects the degree of cultural similarity between these strings. We present different approaches to construct name embeddings from contact lists observed at a large web-mail provider, and evaluate their cultural coherence. We demonstrate that name embeddings strongly encode gender and ethnicity, as well as name popularity. We applied this algorithm to generate imitation names in email contact list challenge. Our controlled user study verified that the proposed technique reduced the attacker's success rate to 26.08%, indistinguishable from random guessing, compared to a success rate of 62.16% from previous name generation algorithms. Finally, we use these embeddings to produce an open synthetic name resource of 1 million names for security applications, constructed to respect both cultural coherence and U.S. census name frequencies.

HACL* is a verified portable C cryptographic library that implements modern cryptographic primitives such as the ChaCha20 and Salsa20 encryption algorithms, Poly1305 and HMAC message authentication, SHA-256 and SHA-512 hash functions, the Curve25519 elliptic curve, and Ed25519 signatures. HACL* is written in the F* programming language and then compiled to readable C code. The F* source code for each cryptographic primitive is verified for memory safety, mitigations against timing side-channels, and functional correctness with respect to a succinct high-level specification of the primitive derived from its published standard. The translation from F* to C preserves these properties and the generated C code can itself be compiled via the CompCert verified C compiler or mainstream compilers like GCC or CLANG. When compiled with GCC on 64-bit platforms, our primitives are as fast as the fastest pure C implementations in OpenSSL and libsodium, significantly faster than the reference C code in TweetNaCl, and between 1.1x-5.7x slower than the fastest hand-optimized vectorized assembly code in SUPERCOP. HACL* implements the NaCl cryptographic API and can be used as a drop-in replacement for NaCl libraries like libsodium and TweetNaCl. HACL* provides the cryptographic components for a new mandatory ciphersuite in TLS 1.3 and is being developed as the main cryptographic provider for the miTLS verified implementation. Primitives from HACL* are also being integrated within Mozilla's NSS cryptographic library. Our results show that writing fast, verified, and usable C cryptographic libraries is now practical.

Domain squatting is a common adversarial practice where attackers register domain names that are purposefully similar to popular domains. In this work, we study a specific type of domain squatting called "combosquatting," in which attackers register domains that combine a popular trademark with one or more phrases (e.g., betterfacebook[.]com, youtube-live[.]com). We perform the first large-scale, empirical study of combosquatting by analyzing more than 468 billion DNS records - collected from passive and active DNS data sources over almost six years. We find that almost 60% of abusive combosquatting domains live for more than 1,000 days, and even worse, we observe increased activity associated with combosquatting year over year. Moreover, we show that combosquatting is used to perform a spectrum of different types of abuse including phishing, social engineering, affiliate abuse, trademark abuse, and even advanced persistent threats. Our results suggest that combosquatting is a real problem that requires increased scrutiny by the security community.

Over recent years lattice-based cryptography has received much attention due to versatile average-case problems like Ring-LWE or Ring-SIS that appear to be intractable by quantum computers. In this work, we evaluate and compare implementations of Ring-LWE encryption and the bimodal lattice signature scheme (BLISS) on an 8-bit Atmel ATxmega128 microcontroller. Our implementation of Ring-LWE encryption provides comprehensive protection against timing side-channels and takes 24.9ms for encryption and 6.7ms for decryption. To compute a BLISS signature, our software takes 317ms and 86ms for verification. These results underline the feasibility of lattice-based cryptography on constrained devices.

The proliferation of mobile technology promotes social activities without time and space limitation. Users share information about their interests and preferences through a social network service, blog, or community. However, sensitive personal information may be exposed with the use of social activities. For example, a specific person can be identified according to exposure of personal information on the web. In this paper, we shows that a nickname that is used in an online community can be tracked by analysis of a user's behavior even though the nickname is changed to avoid identification. Unlike existing studies about user identification in a social network service, we focus on online community, which has not been extensively studied. We analyze characteristics of the online community and propose a method to track a user's nickname change to identify the user. We validate the proposed method using data collected from the online community. Results show that the proposed method can track the user's nickname change and link the old nickname with the new one.

We propose new metrics drawing inspiration from the optimization domain that can be used to characterize the effectiveness of moving target defenses better. Besides that, we propose a Network Neighborhood Partitioning algorithm that can help to measure the influence of MTDs more precisely. The techniques proposed here are generic and could be combined with existing metrics. The obtained results demonstrate how additional information about the effectiveness of defenses can be obtained as well as how network neighborhood partitioning helps to improve the granularity of metrics.

We propose new metrics drawing inspiration from the optimization domain that can be used to characterize the effectiveness of moving target defenses better. Besides that, we propose a Network Neighborhood Partitioning algorithm that can help to measure the influence of MTDs more precisely. The techniques proposed here are generic and could be combined with existing metrics. The obtained results demonstrate how additional information about the effectiveness of defenses can be obtained as well as how network neighborhood partitioning helps to improve the granularity of metrics.

The Cyber Transport Systems (CTSs) have made significant advancement along with the development of the information technology and transportation industries worldwide. The rapid proliferation of cyber transportation technology provides rich information and infinite possibilities for our society to understand and use the complex inherent mechanism, which governs the novel intelligence world. In addition, applying information technology to cyber transportation applications open a range of new application scenarios, such as vehicular safety, energy efficiency, reduced pollution, and intelligent maintenance services. However, while enjoying the services and convenience provided by CTS, users, vehicles, even the systems might lose privacy during information transmitting and processing. This paper summarizes the state-of-art research findings on information privacy issues in a broad range. We firstly introduce the typical types of information and the basic mechanisms of information communication in CTS. Secondly, considering the information privacy issues of CTS, we present the literature on information privacy issues and privacy protection approaches in CTS. Thirdly, we discuss the emerging challenges and the opportunities for the information technology community in CTS.

Emerging technologies are proliferating and the computing profession continues to evolve to embrace the many opportunities and solve the many challenges this brings. Among the challenges is identifying and describing the competencies, responsibilities, and curriculum content needed for cybersecurity. As part of addressing these issues, there are efforts taking place that both improve integration of cybersecurity into the established computing disciplines while other efforts are developing and articulating cybersecurity as a new meta-discipline. The various individual computing disciplines, such as Computer Science, Information Technology, and Information Systems, have increased and improved the amount of cybersecurity in their model curricula. In parallel, organizations such as the Cyber Education Project, an ACM/IEEE Joint Task Force, and the accrediting body ABET are producing such artifacts as a multi-disciplinary Body of Knowledge and accreditation program criteria for cybersecurity writ large. This paper explores these various cybersecurity initiatives from the perspective of the Information Technology discipline, and it addresses the degree to which cybersecurity and Information Technology are both similar and different.

Emerging technologies are proliferating and the computing profession continues to evolve to embrace the many opportunities and solve the many challenges this brings. Among the challenges is identifying and describing the competencies, responsibilities, and curriculum content needed for cybersecurity. As part of addressing these issues, there are efforts taking place that both improve integration of cybersecurity into the established computing disciplines while other efforts are developing and articulating cybersecurity as a new meta-discipline. The various individual computing disciplines, such as Computer Science, Information Technology, and Information Systems, have increased and improved the amount of cybersecurity in their model curricula. In parallel, organizations such as the Cyber Education Project, an ACM/IEEE Joint Task Force, and the accrediting body ABET are producing such artifacts as a multi-disciplinary Body of Knowledge and accreditation program criteria for cybersecurity writ large. This paper explores these various cybersecurity initiatives from the perspective of the Information Technology discipline, and it addresses the degree to which cybersecurity and Information Technology are both similar and different.

Information Security in cloud storage is a key trepidation with regards to Degree of Trust and Cloud Penetration. Cloud user community needs to ascertain performance and security via QoS. Numerous models have been proposed [2] [3] [6][7] to deal with security concerns. Detection and prevention of insider threats are concerns that also need to be tackled. Since the attacker is aware of sensitive information, threats due to cloud insider is a grave concern. In this paper, we have proposed an authentication mechanism, which performs authentication based on verifying facial features of the cloud user, in addition to username and password, thereby acting as two factor authentication. New QoS has been proposed which is capable of monitoring and detection of insider threats using Machine Learning Techniques. KNN Classification Algorithm has been used to classify users into legitimate, possibly legitimate, possibly not legitimate and not legitimate groups to verify image authenticity to conclude, whether there is any possible insider threat. A threat detection model has also been proposed for insider threats, which utilizes Facial recognition and Monitoring models. Security Method put forth in [6] [7] is honed to include threat detection QoS to earn higher degree of trust from cloud user community. As a recommendation, Threat detection module should be harnessed in private cloud deployments like Defense and Pharma applications. Experimentation has been conducted using open source Machine Learning libraries and results have been attached in this paper.

The performance evaluation of distribution network operators is essential for the electrical utilities to know how prepared the operators are to execute their operation standards and rules, searching for minimizing the time of power outage, after some contingency. The performance of operators can be evaluated by the impact of their actions on several technical and economic indicators of the distribution system. This issue is a complex problem, whose solution involves necessarily some expertise and a multi-criteria evaluation. This paper presents a Tutorial Expert System (TES) for performance evaluation of electrical distribution network operators after a given contingency in the electrical network. The proposed TES guides the evaluation process, taking into account technical, economic and personal criteria, aiding the quantification of these criteria. A case study based on real data demonstrates the applicability of the performance evaluation procedure of distribution network operators.

We have recently seen an increasing number of attacks that are distributed, and span an entire wide area network (WAN). Today, typically, intrusion detection systems (IDSs) are deployed at enterprise scale and cannot handle attacks that cover a WAN. Moreover, such IDSs are implemented at a single entity that expects to look at all packets to determine an intrusion. Transferring copies of raw packets to centralized engines for analysis in a WAN can significantly impact both network performance and detection accuracy. In this paper, we propose Jaal, a framework for achieving accurate network intrusion detection at scale. The key idea in Jaal is to monitor traffic and construct in-network packet summaries. The summaries are then processed centrally to detect attacks with high accuracy. The main challenges that we address are (a) creating summaries that are concise, but sufficient to draw highly accurate inferences and (b) transforming traditional IDS rules to handle summaries instead of raw packets. We implement Jaal on a large scale SDN testbed. We show that on average Jaal yields a detection accuracy of about 98%, which is the highest reported for ISP scale network intrusion detection. At the same time, the overhead associated with transferring summaries to the central inference engine is only about 35% of what is consumed if raw packets are transferred.

Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler on representative cryptographic routines and conclude that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks). We also demonstrate the effectiveness of the verification tools on a large set of cryptographic routines.

The large scale and high complexity of modern software systems make perfectly precise static code analysis (SCA) infeasible. Therefore SCA tools often over-approximate, so not to miss any real problems. This, however, comes at the expense of raising false alarms, which, in practice, reduces the usability of these tools. To partially address this problem, we propose a novel learning process whose goal is to discover program structures that cause a given SCA tool to emit false error reports, and then to use this information to predict whether a new error report is likely to be a false positive as well. To do this, we first preprocess code to isolate the locations that are related to the error report. Then, we apply machine learning techniques to the preprocessed code to discover correlations and to learn a classifier. We evaluated this approach in an initial case study of a widely-used SCA tool for Java. Our results showed that for our dataset we could accurately classify a large majority of false positive error reports. Moreover, we identified some common coding patterns that led to false positive errors. We believe that SCA developers may be able to redesign their methods to address these patterns and reduce false positive error reports.

In this paper1 is proposed a graph model, designed to solve security challenges of information systems (IS). The model allows to describe information systems at two levels. The first is the transport layer, represented by the graph, and the second is functional level, represented by the semantic network. Proposed model uses "subject-object" terms to establish a security policy. Based on the proposed model, one can define information system security features location, and choose their deployment in the best way. In addition, it is possible to observe data access control security features inadequacy and calculate security value for the each IS node. Novelty of this paper is that one can get numerical evaluation of IS security according to its nodes communications and network structure.

Weak security, excessive personal data collection for user profiling, and a poor user experience are just a few of the many problems that mobile authentication solutions suffer from. Despite being an interesting platform, mobile devices are still not being used to their full potential for authentication. n-Auth is a firm step in unlocking the full potential of mobile devices in authentication, by improving both security and usability whilst respecting the privacy of the user. Our focus is on the combined usage of several strong cryptographic techniques with secure HCI design principles to achieve a better user experience. We specified and built n-Auth, for which robust Android and iOS apps are openly available through the official stores.

By migrating their data and operations to the cloud, enterprises are able to gain significant benefits in terms of cost savings, increased availability, agility and productivity. Yet, the shared and on-demand nature of the cloud paradigm introduces a new breed of security threats that generally deter stakeholders from relinquishing control of their critical assets to third-party cloud providers. One way to thwart these threats is to instill suitable access control policies into cloud services that protect these assets. Nevertheless, the dynamic nature of cloud environments calls for policies that are able to incorporate a potentially complex body of contextual knowledge. This complexity is further amplified by the interplay that inevitably occurs between the different policies, as well as by the dynamically-evolving nature of an organisation's business and security needs. We argue that one way to tame this complexity is to devise a generic framework that facilitates the governance of policies. This paper presents a particular aspect of such a framework, namely an approach to determining the repercussions that policy retirement actions have on the overall protection of critical assets in the cloud.

User's personal portable devices such as smartphone, tablet and laptop require continuous authentication of the user to prevent against illegitimate access to the device and personal data. Current authentication techniques require users to enter password or scan fingerprint, making frequent access to the devices inconvenient. In this work, we propose to exploit user's on-body wearable devices to detect their proximity from her portable devices, and use the proximity for continuous authentication of the portable devices. We present PCASA which utilizes acoustic communication for secure proximity estimation with sub-meter level accuracy. PCASA uses Differential Pulse Position Modulation scheme that modulates data through varying the silence period between acoustic pulses to ensure energy efficiency even when authentication operation is being performed once every second. It yields an secure and accurate distance estimation even when user is mobile by utilizing Doppler effect for mobility speed estimation. We evaluate PCASA using smartphone and smartwatches, and show that it supports up to 34 hours of continuous authentication with a fully charged battery.