Biblio

Online controlled experiments (a.k.a. A/B testing) have been used as the mantra for data-driven decision making on feature changing and product shipping in many Internet companies. However, it is still a great challenge to systematically measure how every code or feature change impacts millions of users with great heterogeneity (e.g. countries, ages, devices). The most commonly used A/B testing framework in many companies is based on Average Treatment Effect (ATE), which cannot detect the heterogeneity of treatment effect on users with different characteristics. In this paper, we propose statistical methods that can systematically and accurately identify Heterogeneous Treatment Effect (HTE) of any user cohort of interest (e.g. mobile device type, country), and determine which factors (e.g. age, gender) of users contribute to the heterogeneity of the treatment effect in an A/B test. By applying these methods on both simulation data and real-world experimentation data, we show how they work robustly with controlled low False Discover Rate (FDR), and at the same time, provides us with useful insights about the heterogeneity of identified user groups. We have deployed a toolkit based on these methods, and have used it to measure the Heterogeneous Treatment Effect of many A/B tests at Snap.

In this paper, we explore the use of the Stellar Consensus Protocol (SCP) and its Federated Byzantine Agreement (FBA) algorithm for ensuring trust and reputation between federated, cloud-based platform instances (nodes) and their participants. Our approach is grounded on federated consensus mechanisms, which promise data quality managed through computational trust and data replication, without a centralized authority. We perform our experimentation on the ground of the NIMBLE cloud manufacturing platform, which is designed to support growth of B2B digital manufacturing communities and their businesses through federated platform services, managed by peer-to-peer networks. We discuss the message exchange flow between the NIMBLE application logic and Stellar consensus logic.

Users have accumulated years of personal data in cloud storage, creating potential privacy and security risks. This agglomeration includes files retained or shared with others simply out of momentum, rather than intention. We presented 100 online-survey participants with a stratified sample of 10 files currently stored in their own Dropbox or Google Drive accounts. We asked about the origin of each file, whether the participant remembered that file was stored there, and, when applicable, about that file's sharing status. We also recorded participants' preferences moving forward for keeping, deleting, or encrypting those files, as well as adjusting sharing settings. Participants had forgotten that half of the files they saw were in the cloud. Overall, 83% of participants wanted to delete at least one file they saw, while 13% wanted to unshare at least one file. Our combined results suggest directions for retrospective cloud data management.

Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found. 

As a decentralized and distributed secure storage technology, the notion of blockchain is now widely used for electronic trading in finance, for issuing digital certificates, for copyrights management, and for many other security-critical applications. With applications in so many domains with high-assurance requirements, the formalization and verification of safety and security properties of blockchain becomes essential, and the aim of the present paper. We present the model-based formalization, simulation and verification of a blockchain protocol by using the SDL formalism of Telelogic Tau. We consider the hierarchical and modular SDL model of the blockchain protocol and exercise a methodology to formally simulate and verify it. This way, we show how to effectively increase the security and safety of blockchain in order to meet high assurance requirements demanded by its application domains. Our work also provides effective support for assessing different network consensus algorithms, which are key components in blockchain protocols, as well as on the topology of blockchain networks. In conclusion, our approach contributes to setting up a verification methodology for future blockchain standards in digital trading.

Global Platform (GP)1 specifications accepted as de facto industry standards are widely used for the development of embedded operating system running on secure chip devices. A promising approach to demonstrating the implementation of an OS meets its specification is formal verification. However, most previous work on operating system verification targets high-level source programs proving the correspondence between abstract specification and high-level implementation but ignoring the machine-code level implementation parts. Thus, this kind of correspondence proofs stay in a shallow level. In this paper, we present a novel methodology for formal specifying and certifying the implementation of an embedded operating system strictly follows the GP specification. We establish a multiple abstraction layers framework that has four layers, from up to down, which are Formal Global Platform Layer (FGPL), Formal Specification High Layer (FSHL), Formal Specification Low Layer (FSLL) and Formal Assembly Machine Layer (FAML). To demonstrate the effectiveness of our methodology, we take the communication module of our Trust-E operating system (running on an extended CompCert ARM assembly machine model) as a case study and have successfully constructed a multi-layered proof, fully formalized in the Coq proof assistant. Some parts of the module are written in C and some are written in assembly; we certify that all codes implementation follow Global Platform specification.

Control-hijacking attacks include code injection attacks and code reuse attacks. In recent years, with the emergence of the defense mechanism data-execution prevention(DEP), code reuse attacks have become mainstream, such as return-oriented programming(ROP), Jump-Oriented Programming(JOP), and Counterfeit Object-oriented Programming(COOP). And a series of defensive measures have been proposed, such as DEP, address space layout randomization (ASLR), coarse-grained Control-Flow Integrity(CFI) and fine-grained CFI. In this paper, we propose a new attack called function-oriented programming(FOP) to construct malicious program behavior. FOP takes advantage of the existing function of the C program to induce attack. We propose concrete algorithms for FOP gadgets and build a tool to identify FOP gadgets. FOP can successfully bypass coarse-grained CFI, and FOP also can bypass some existing fine-grained CFI technologies, such as shadow stack technology. We show a real-world attack for proftpd1.3.0 server in the Linux x64 environment. We believe that the FOP attack will encourage people to come up with more effective defense measures.

This paper presents a control strategy for Cyber-Physical System defense developed in the framework of the European Project ATENA, that concerns Critical Infrastructure (CI) protection. The aim of the controller is to find the optimal security configuration, in terms of countermeasures to implement, in order to address the system vulnerabilities. The attack/defense problem is modeled as a multi-agent general sum game, where the aim of the defender is to prevent the most damage possible by finding an optimal trade-off between prevention actions and their costs. The problem is solved utilizing Reinforcement Learning and simulation results provide a proof of the proposed concept, showing how the defender of the protected CI is able to minimize the damage caused by his her opponents by finding the Nash equilibrium of the game in the zero-sum variant, and, in a more general scenario, by driving the attacker in the position where the damage she/he can cause to the infrastructure is lower than the cost it has to sustain to enforce her/his attack strategy.

In the past decades, static code analysis has become a prevalent means to detect bugs and security vulnerabilities in software systems. As software becomes more complex, analysis tools also report lists of increasingly complex warnings that developers need to address on a daily basis. The novel insight we present in this work is that static analysis tools and video games both require users to take on repetitive and challenging tasks. Importantly, though, while good video games manage to keep players engaged, static analysis tools are notorious for their lacking user experience, which prevents developers from using them to their full potential, frequently resulting in dissatisfaction and even tool abandonment. We show parallels between gaming and using static analysis tools, and advocate that the user-experience issues of analysis tools can be addressed by looking at the analysis tooling system as a whole, and by integrating gaming elements that keep users engaged, such as providing immediate and clear feedback, collaborative problem solving, or motivators such as points and badges.

In this paper we show how genetic algorithms can be effectively applied to study the security of arbitrary quantum key distribution (QKD) protocols when faced with adversaries limited to current-day technology. We compare two approaches, both of which take into account practical limitations on the quantum power of an adversary (which can be specified by the user). Our system can be used to determine upper-bounds on noise tolerances of novel QKD protocols in this scenario, thus making it a useful tool for researchers. We compare our algorithm's results with current known numerical results, and also evaluate it on newer, more complex, protocols where no results are currently known.

Smart industrial control systems (e.g., smart grid, oil and gas systems, transportation systems) are connected to the internet, and have the capability to collect and transmit data; as such, they are part of the IoT. The data collected can be used to improve services; however, there are serious privacy risks. This concern is usually addressed by means of privacy policies, but it is often difficult to understand the scope and consequences of such policies. Better tools to visualise and analyse data collection policies are needed. Graph-based modelling tools have been used to analyse complex systems in other domains. In this paper, we apply this technique to IoT data-collection policy analysis and visualisation. We describe graphical representations of category-based data collection policies and show that a graph-based policy language is a powerful tool not only to specify and visualise the policy, but also to analyse policy properties. We illustrate the approach with a simple example in the context of a chemical plant with a truck monitoring system. We also consider policy administration: we propose a classification of queries to help administrators analyse policies, and we show how the queries can be answered using our technique.

A Mobile ad hoc network (MANET) is a set of nodes that communicate together in a cooperative way using the wireless medium, and without any central administration. Due to its inherent open nature and the lack of infrastructure, security is a complicated issue compared to other networks. That is, these networks are vulnerable to a a wide range of attacks at different network layers. At the network level, malicious nodes can perform several attacks ranging from passive eavesdropping to active interfering. Wormhole is an example of severe attack that has attracted much attention recently. It involves the redirection of traffic between two end-nodes through a Wormhole tunnel, and manipulates the routing algorithm to give illusion that nodes located far from each other are neighbors. To handle with this issue, we propose a novel detection model to allow a node to check whether a presumed shortest path contains a Wormhole tunnel or not. Our approach is based on the fact that the Wormhole tunnel reduces significantly the length of the paths passing through it.

We propose a Centralized Tree based Diffie-Hellman (CTDH) protocol for wireless mesh networks, which take into account the characteristics of mesh network operations, wireless routers and mobile devices. Performance analysis shows that CTDH is more efficient than the Tree-Based Group Diffie-Hellman Protocol (TGDH).

With the development of cloud computing the topology properties of data center network are important to the computing resources. Recently a data center network structure - BCCC is proposed, which is recursively built structure with many good properties. and expandability. The Hamiltonian and expandability in data center network structure plays an extremely important role in network communication. This paper described the Hamiltonian and expandability of the expandable data center network for BCCC structure, the important role of Hamiltonian and expandability in network traffic.

Vulnerabilities in hypervisors are crucial in multi-tenant clouds and attractive for attackers because a vulnerability in the hypervisor can undermine all the virtual machine (VM) security. This paper focuses on vulnerabilities in instruction emulators inside hypervisors. Vulnerabilities in instruction emulators are not rare; CVE-2017-2583, CVE-2016-9756, CVE-2015-0239, CVE-2014-3647, to name a few. For backward compatibility with legacy x86 CPUs, conventional hypervisors emulate arbitrary instructions at any time if requested. This design leads to a large attack surface, making it hard to get rid of vulnerabilities in the emulator. This paper proposes FWinst that narrows the attack surface against vulnerabilities in the emulator. The key insight behind FWinst is that the emulator should emulate only a small subset of instructions, depending on the underlying CPU micro-architecture and the hypervisor configuration. FWinst recognizes emulation contexts in which the instruction emulator is invoked, and identifies a legitimate subset of instructions that are allowed to be emulated in the current context. By filtering out illegitimate instructions, FWinst narrows the attack surface. In particular, FWinst is effective on recent x86 micro-architectures because the legitimate subset becomes very small. Our experimental results demonstrate FWinst prevents existing vulnerabilities in the emulator from being exploited on Westmere micro-architecture, and the runtime overhead is negligible.

Return Oriented Programming is one of the most important software security challenges nowadays. It exploits memory vulnerabilities to control the state of the program and hijacks its control flow. Existing defenses usually focus on how to protect the control flow or face the challenge of how to maintain the taint markings for memory data. In this paper, we directly focus on the adversary-controlled states, simplify the classic dynamic taint analysis method to only track registers and propose Hardware-based Adversary-controlled States Tracking (HAST). HAST dynamically tracks registers that may be controlled by the adversary to detect ROP attack. It is transparent to user application and makes few modifications to existing hardware. Our evaluation demonstrates that HAST will introduce almost no performance overhead and can effectively detect ROP attacks without false positives on the tested common Linux applications.

The NEREIDA wave generation power plant installed in Mutriku, Spain is a multiple Oscillating Water Column (OWC) plant. The power takeoff consists of a Wells turbine coupled to a Doubly Fed Induction Generator (DFIG). The stalling behavior present in the Wells turbine limits the generated power. This paper presents the modeling and a Harmony Search Algorithm-based airflow control of the OWC. The Harmony Search Algorithm (HSA) is proposed to help overcome the limitations of a traditionally tuned PID. An investigation between HSA-tuned controller and the traditionally tuned controller has been performed. Results of the controlled and uncontrolled plant prove the effectiveness of the airflow control and the superiority of the HSA-tuned controller.

ARM has become the leading processor architecture for mobile and IoT devices, while it has recently started claiming a bigger slice of the server market pie as well. As such, it will not be long before malware more regularly target the ARM architecture. Therefore, the stealthy operation of Virtual Machine Introspection (VMI) is an obligation to successfully analyze and proactively mitigate this growing threat. Stealthy VMI has proven itself perfectly suitable for malware analysis on Intel's architecture, yet, it often lacks the foundation required to be equally effective on ARM.

ARM devices (mobile phone, IoT devices) are getting more popular in our daily life due to the low power consumption and cost. These devices carry a huge number of user's private information, which attracts attackers' attention and increase the security risk. The operating systems (e.g., Android, Linux) works out many memory data protection strategies on user's private information. However, the monolithic OS may contain security vulnerabilities that are exploited by the attacker to get root or even kernel privilege. Once the kernel privilege is obtained by the attacker, all data protection strategies will be gone and user's private information can be taken away. In this paper, we propose a hardened memory data protection framework called H-Securebox to defeat kernel-level memory data stolen attacks. H-Securebox leverages ARM hardware virtualization technique to protect the data on the memory with hypervisor privilege. We designed three types H-Securebox for programing developers to use. Although the attacker may have kernel privilege, she can not touch private data inside H-Securebox, since hypervisor privilege is higher than kernel privilege. With the implementation of H-Securebox system assisting by a tiny hypervisor on Raspberry Pi2 development board, we measure the performance overhead of our system and do the security evaluations. The results positively show that the overhead is negligible and the malicious application with root or kernel privilege can not access the private data protected by our system.

Third-party software daemons called host agents are increasingly responsible for a modern host's security, automation, and monitoring tasks. Because of their location within the host, these agents are at risk of manipulation by malware and users. Additionally, in virtualized environments where multiple adjacent guests each run their own set of agents, the cumulative resources that agents consume adds up rapidly. Consolidating agents onto the hypervisor can address these problems, but places a technical burden on agent developers. This work presents a development methodology to re-engineer a host agent in to a hyperagent, an out-of-guest agent that gains unique hypervisor-based advantages while retaining its original in-guest capabilities. This three-phase methodology makes integrating Virtual Machine Introspection (VMI) functionality in to existing code easier and more accessible, minimizing an agent developer's re-engineering effort. The benefits of hyperagents are illustrated by porting the GRR live forensics agent, which retains 89% of its codebase, uses 40% less memory than its in-guest counterparts, and enables a 4.9x speedup for a representative data-intensive workload. This work shows that a conventional off-the-shelf host agent can be feasibly transformed into a hyperagent and provide a powerful, efficient tool for defending virtualized systems.

This paper presents HyperFlow, a processor that enforces secure information flow, including control over timing channels. The design and implementation of HyperFlow offer security assurance because it is implemented using a security-typed hardware description language that enforces secure information flow. Unlike prior processors that aim to enforce simple information-flow policies such as noninterference, HyperFlow allows complex information flow policies that can be configured at run time. Its fine-grained, decentralized information flow mechanisms allow controlled communication among mutually distrusting processes and system calls into different security domains. We address the significant challenges in designing such a processor architecture with contributions in both the hardware architecture and the security type system. The paper discusses the architecture decisions that make the processor secure and describes ChiselFlow, a new secure hardware description language supporting lightweight information-flow enforcement. The HyperFlow architecture is prototyped on a full-featured processor that offers a complete RISC-V instruction set, and is shown to add moderate overhead to area and performance.

This computer era leads human to interact with computers and networks but there is no such solution to get rid of security problems. Securities threats misleads internet, we are sometimes losing our hope and reliability with many server based access. Even though many more crypto algorithms are coming for integrity and authentic data in computer access still there is a non reliable threat penetrates inconsistent vulnerabilities in networks. These vulnerable sites are taking control over the user's computer and doing harmful actions without user's privileges. Though Firewalls and protocols may support our browsers via setting certain rules, still our system couldn't support for data reliability and confidentiality. Since these problems are based on network access, lets we consider TCP/IP parameters as a dataset for analysis. By doing preprocess of TCP/IP packets we can build sovereign model on data set and clump cluster. Further the data set gets classified into regular traffic pattern and anonymous pattern using KNN classification algorithm. Based on obtained pattern for normal and threats data sets, security devices and system will set rules and guidelines to learn by it to take needed stroke. This paper analysis the computer to learn security actions from the given data sets which already exist in the previous happens.

Ubiquitous Healthcare System (U-Healthcare) is a well-known application of wireless sensor networking (WSN). In this system, the sensors take less power for operating the function. As the data transfers between sensor and other stations is sensitive so there needs to provide a security scheme. Due to the low life of sensor nodes in Wireless Sensor Networks (WSN), asymmetric key based security (AKS) architecture is always considered as unsuitable for these types of networks. Several papers have been published in recent past years regarding how to incorporate AKS in WSN, Haque et al's Asymmetric key based Architecture (AKA) is one of them. But later it is found that this system has authentication problem and therefore prone to man-in-the-middle (MITM) attack, furthermore it is not a truly asymmetric based scheme. We address these issues in this paper and proposed a complete asymmetric approach using PEKS-PM (proposed by Pham in [8]) to remove impersonation attack. We also found some other vulnerabilities in the original AKA system and proposed solutions, therefore making it a better and enhanced asymmetric key based architecture.

This paper presents some verifications and improved considerations of NAND PUF, which was introduced recently [1]. For embedded system such as IC cards, the secret data in memory is vulnerable, so it has to be encrypted and secured. PUF circuit is sensitive to environmental condition, especially in the temperature range influences and variations of current and voltages. This proposed bank IC card would be operated in AB class standard, i.e. voltage would be constant except for power mode changing. Nevertheless, operational temperatures may vary such as the situation of outdoor ATM. Thus, this paper presented some results of our PUF work in Cadence, also on FPGA board. Around 5ns is spent for stabilization of our PUF output that is under variance temperature when power mode changes. Inter Hamming distances is 48.9%, very near to uniqueness and robustness value, that our PUF is feasible to use in bankcard. The maximum error rates are HDintra(0$^\circ$C) = 3.9961 and HDintra(80$^\circ$C) = 3.9916 where at antipoles, while the minimum error rate is HDintra(20$^\circ$C) = 2.9 at room temperature. For improvement, Repetition, LDPC and SEC-DED codes are considered that would eliminate error rates.

Recent work, including ZKBoo, ZKB++, and Ligero, has developed efficient non-interactive zero-knowledge proofs of knowledge (NIZKPoKs) for Boolean circuits based on symmetric-key primitives alone, using the "MPC-in-the-head" paradigm of Ishai et al. We show how to instantiate this paradigm with MPC protocols in the preprocessing model; once optimized, this results in an NIZKPoK with shorter proofs (and comparable computation) as in prior work for circuits containing roughly 300–100,000 AND\textasciitildegates. In contrast to prior work, our NIZKPoK also supports witness-independent preprocessing, which allows the prover to shift most of its work to an offline phase before the witness is known. We use our NIZKPoK to construct a signature scheme based only on symmetric-key primitives (and hence with "post-quantum" security). The resulting scheme has shorter signatures than the scheme built using ZKB++ (and comparable signing/verification time), and is even competitive with hash-based signature schemes. To further highlight the flexibility and power of our NIZKPoK, we also use it to build efficient ring and group signatures based on symmetric-key primitives alone. To our knowledge, the resulting schemes are the most efficient constructions of these primitives that offer post-quantum security.