Biblio

The SPECTRE family of speculative execution attacks has required a rethinking of formal methods for security. Approaches based on operational speculative semantics have made initial inroads towards finding vulnerable code and validating defenses. However, with each new attack grows the amount of microarchitectural detail that has to be integrated into the underlying semantics. We propose an alternative, lightweight and axiomatic approach to specifying speculative semantics that relies on insights from memory models for concurrency. We use the CAT modeling language for memory consistency to specify execution models that capture speculative control flow, store-to-load forwarding, predictive store forwarding, and memory ordering machine clears. We present a bounded model checking framework parameterized by our speculative CAT models and evaluate its implementation against the state of the art. Due to the axiomatic approach, our models can be rapidly extended to allow our framework to detect new types of attacks and validate defenses against them.

Given the COVID-19 pandemic, this paper aims at providing a full-process information system to support the detection of pathogens for a large range of populations, satisfying the requirements of light weight, low cost, high concurrency, high reliability, quick response, and high security. The project includes functional modules such as sample collection, sample transfer, sample reception, laboratory testing, test result inquiry, pandemic analysis, and monitoring. The progress and efficiency of each collection point as well as the status of sample transfer, reception, and laboratory testing are all monitored in real time, in order to support the comprehensive surveillance of the pandemic situation and support the dynamic deployment of pandemic prevention resources in a timely and effective manner. Deployed on a cloud platform, this system can satisfy ultra-high concurrent data collection requirements with 20 million collections per day and a maximum of 5 million collections per hour, due to its advantages of high concurrency, elasticity, security, and manageability. This system has also been widely used in Jiangsu, Shaanxi provinces, for the prevention and control of COVID-19 pandemic. Over 100 million NAT data have been collected nationwide, providing strong informational support for scientific and reasonable formulation and execution of COVID-19 prevention plans.

In the process of crowdsourced testing service, the intellectual property of crowdsourced testing has been faced with problems such as code plagiarism, difficulties in confirming rights and unreliability of data. Blockchain is a decentralized, tamper-proof distributed ledger, which can help solve current problems. This paper proposes an intellectual property right confirmation system oriented to crowdsourced testing services, combined with blockchain, IPFS (Interplanetary file system), digital signature, code similarity detection to realize the confirmation of crowdsourced testing intellectual property. The performance test shows that the system can meet the requirements of normal crowdsourcing business as well as high concurrency situations.

With the rapid development of Internet Technology in recent years, the demand for security support for complex applications is becoming stronger and stronger. Intel Software Guard Extensions (Intel SGX) is created as an extension of Intel Systems to enhance software security. Intel SGX allows application developers to create so-called enclave. Sensitive application code and data are encapsulated in Trusted Execution Environment (TEE) by enclave. TEE is completely isolated from other applications, operating systems, and administrative programs. Enclave is the core structure of Intel SGX Technology. Enclave supports multi-threading. Thread Control Structure (TCS) stores special information for restoring enclave threads when entering or exiting enclave. Each execution thread in enclave is associated with a TCS. This paper analyzes and verifies the possible security risks of enclave under concurrent conditions. It is found that in the case of multithread concurrency, a single enclave cannot resist flooding attacks, and related threads also throw TCS exception codes.

Concurrency vulnerabilities caused by synchronization problems will occur in the execution of multi-threaded programs, and the emergence of concurrency vulnerabilities often cause great threats to the system. Once the concurrency vulnerabilities are exploited, the system will suffer various attacks, seriously affecting its availability, confidentiality and security. In this paper, we extract 839 concurrency vulnerabilities from Common Vulnerabilities and Exposures (CVE), and conduct a comprehensive analysis of the trend, classifications, causes, severity, and impact. Finally, we obtained some findings: 1) From 1999 to 2021, the number of concurrency vulnerabilities disclosures show an overall upward trend. 2) In the distribution of concurrency vulnerability, race condition accounts for the largest proportion. 3) The overall severity of concurrency vulnerabilities is medium risk. 4) The number of concurrency vulnerabilities that can be exploited for local access and network access is almost equal, and nearly half of the concurrency vulnerabilities (377/839) can be accessed remotely. 5) The access complexity of 571 concurrency vulnerabilities is medium, and the number of concurrency vulnerabilities with high or low access complexity is almost equal. The results obtained through the empirical study can provide more support and guidance for research in the field of concurrency vulnerabilities.

With the development of cloud computing, remote attestation of virtual machines has received extensive attention. However, the current schemes mainly concentrate on the single prover, and the attestation of a large-scale virtualization environment will cause TPM bottleneck and network congestion, resulting in low efficiency of attestation. This paper proposes CloudTA, an extensible remote attestation architecture. CloudTA groups all virtual machines on each cloud server and introduces an integrity measurement group (IMG) to measure virtual machines and generate trusted evidence by a group. Subsequently, the cloud server reports the physical platform and VM group's trusted evidence for group verification, reducing latency and improving efficiency. Besides, CloudTA designs a hybrid high concurrency communication framework for supporting remote attestation of large-scale virtual machines by combining active requests and periodic reports. The evaluation results suggest that CloudTA has good efficiency and scalability and can support remote attestation of ten thousand virtual machines.

In this paper, we highlight a fundamental vulnerability associated with the widely adopted “Just Tap” push-based authentication in the face of a concurrency attack, and propose the method REPLICATE, a redesign to counter this vulnerability. In the concurrency attack, the attacker launches the login session at the same time the user initiates a session, and the user may be fooled, with high likelihood, into accepting the push notification which corresponds to the attacker's session, thinking it is their own. The attack stems from the fact that the login notification is not explicitly mapped to the login session running on the browser in the Just Tap approach. REPLICATE attempts to address this fundamental flaw by having the user approve the login attempt by replicating the information presented on the browser session over to the login notification, such as by moving a key in a particular direction, choosing a particular shape, etc. We report on the design and a systematic usability study of REPLICATE. Even without being aware of the vulnerability, in general, participants placed multiple variants of REPLICATE in competition to the Just Tap and fairly above PIN-based authentication.

Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means of type checking), but they are inherently restrictive in the kind of programs they support. Program logics support challenging programs, but they typically require significant human assistance, and cannot handle modules or higher-order programs.To connect these two approaches, we present SeLoC—a separation logic for non-interference, on top of which we build a type system using the technique of logical relations. By building a type system on top of separation logic, we can compositionally verify programs that consist of typed and untyped parts. The former parts are verified through type checking, while the latter parts are verified through manual proof.The core technical contribution of SeLoC is a relational form of weakest preconditions that can track information flow using separation logic resources. SeLoC is fully machine-checked, and built on top of the Iris framework for concurrent separation logic in Coq. The integration with Iris provides seamless support for fine-grained concurrency, which was beyond the reach of prior type systems and program logics for non-interference.

Smart Contracts based cryptocurrencies such as Ethereum are becoming increasingly popular in various domains: but with this increase in popularity comes a significant decrease in throughput and efficiency. Smart Contracts are executed by every miner in the system serially without any parallelism, both inter and intra-Smart Contracts. Such a serial execution inhibits the scalability required to obtain extremely high throughput pertaining to computationally intensive tasks deployed with such Smart Contracts. While significant advancements have been made in the field of concurrency, from GPU architectures that enable massively parallel computation to tools such as MapRe-duce that distributed computing to several nodes connected in the system to achieve higher performance in distributed systems, none are incorporated in blockchain-based distributed computing. The team proposes a novel blockchain that allows public nodes in a permission-independent blockchain to deploy and run Smart Contracts that provide concurrency-related functionalities within the Smart Contract framework. In this paper, the researchers present “ConCurrency,” a blockchain network capable of handling big data-based computations. The technique is based on currently used distributed system paradigms, such as MapReduce, while also allowing for fundamental parallelly computable problems. Concurrency is achieved using a sharding protocol incorporated with consensus mechanisms to ensure high scalability, high reliability, and better efficiency. A detailed methodology and a comprehensive analysis of the proposed blockchain further indicate a significant increase in throughput for parallelly computable tasks, as detailed in this paper.

Realizing flow security in a concurrent environment is extremely challenging, primarily due to non-deterministic nature of execution. The difficulty is further exacerbated from a security angle if sequential threads disclose control locations through publicly observable statements like print, sleep, delay, etc. Such observations lead to internal and external timing attacks. Inspired by previous works that use classical Hoare style proof systems for establishing correctness of distributed (real-time) programs, in this paper, we describe a method for finding information leaks in concurrent programs through the introduction of leaky assertions at observable program points. Specifying leaky assertions akin to classic assertions, we demonstrate how information leaks can be detected in a concurrent context. To our knowledge, this is the first such work that enables integration of different notions of non-interference used in functional and security context. While the approach is sound and relatively complete in the classic sense, it enables the use of algorithmic techniques that enable programmers to come up with leaky assertions that enable checking for information leaks in sensitive applications.

A number of approaches have been developed for analysing information flow in concurrent programs in a compositional manner, i.e., in terms of one thread at a time. Early approaches modelled the behaviour of a given thread's environment using simple read and write permissions on variables, or by associating specific behaviour with whether or not locks are held. Recent approaches allow more general representations of environmental behaviour, increasing applicability. This, however, comes at a cost. These approaches analyse the code in a forwards direction, from the start of the program to the end, constructing the program's entire state after each instruction. This process needs to take into account the environmental influence on all shared variables of the program. When environmental influence is modelled in a general way, this leads to increased complexity, hindering automation of the analysis. In this paper, we present a compositional information flow analysis for concurrent systems which is the first to support a general representation of environmental behaviour and be automated within a theorem prover. Our approach analyses the code in a backwards direction, from the end of the program to the start. Rather than constructing the entire state at each instruction, it generates only the security-related proof obligations. These are, in general, much simpler, referring to only a fraction of the program's shared variables and thus reducing the complexity introduced by environmental behaviour. For increased applicability, our approach analyses value-dependent information flow, where the security classification of a variable may depend on the current state. The resulting logic has been proved sound within the theorem prover Isabelle/HOL.

Concurrency programs often induce buggy results due to the unexpected interaction among threads. The detection of these concurrency bugs costs a lot because they usually appear under a specific execution trace. How to virtually explore different thread schedules to detect concurrency bugs efficiently is an important research topic. Many techniques have been proposed, including lightweight techniques like adaptive randomized scheduling (ARS) and heavyweight techniques like maximal causality reduction (MCR). Compared to heavyweight techniques, ARS is efficient in exploring different schedulings and achieves state-of-the-art performance. However, it will lead to explore large numbers of redundant thread schedulings, which will reduce the efficiency. Moreover, it suffers from the “cold start” issue, when little information is available to guide the distance calculation at the beginning of the exploration. In this work, we propose a Heuristic-Enhanced Adaptive Randomized Scheduling (HARS) algorithm, which improves ARS to detect concurrency bugs guided with novel distance metrics and heuristics obtained from existing research findings. Compared with the adaptive randomized scheduling method, it can more effectively distinguish the traces that may contain concurrency bugs and avoid redundant schedules, thus exploring diverse thread schedules effectively. We conduct an evaluation on 45 concurrency Java programs. The evaluation results show that our algorithm performs more stably in terms of effectiveness and efficiency in detecting concurrency bugs. Notably, HARS detects hard-to-expose bugs more effectively, where the buggy traces are rare or the bug triggering conditions are tricky.

Reducing latency in inter-process/inter-thread communication is one of the key challenges in parallel and distributed computing. This is because as the number of threads in an application increases, the communication overhead also increases. Moreover, the presence of background load further increases the latency. Reducing communication latency can have a significant impact on multi-threaded application performance in multi-core environments. In a wide-range of applications that utilize queueing mechanism, inter-process/ inter-thread communication typically involves enqueuing and dequeuing. This paper presents a queueing techniques called eLCRQ, which is a lock-free block-when-necessary multi-producer multi-consumer (MPMC) FIFO queue. It is designed for scenarios where the queue can randomly and frequently become empty during runtime. By combining lock-free performance with blocking resource efficiency, it delivers improved performance. Specifically, it results in a 1.7X reduction in latency and a 2.3X reduction in CPU usage when compared to existing message-passing mechanisms including PIPE and Sockets while running on multi-core Linux based systems. The proposed scheme also provides a 3.4X decrease in CPU usage while maintaining comparable latency when compared to other (MPMC) lock-free queues in low load scenarios. Our work is based on open-source Linux and support libraries.

As portals to the Internet, web browsers constitute prominent targets for attacks. Existing defenses that redefine web APIs typically capture information related to a single JavaScript function. Thus, they fail to defend against the so-called web concurrency attacks that use multiple interleaved functions to trigger a browser vulnerability. In this paper, we propose JSKernel, the first generic framework that introduces a kernel concept into JavaScript to defend against web concurrency attacks. The JavaScript kernel, inspired from operating system concepts, enforces the execution order of JavaScript events and threads to fortify security. We implement a prototype of JSKernel deployable as add-on extensions to three widely used web browsers, namely Google Chrome, Mozilla Firefox, and Microsoft Edge. These open-source extensions are available at (https://github.com/jskernel2019/jskernel) along with a usability demo at (https://jskernel2019.github.io/). Our evaluation shows the prototype to be robust to web concurrency attacks, fast, and backward compatible with legacy websites.

Data races occur when two threads fail to use proper synchronization when accessing shared data. In kernel file systems, which are highly concurrent by design, data races are common mistakes and often wreak havoc on the users, causing inconsistent states or data losses. Prior fuzzing practices on file systems have been effective in uncovering hundreds of bugs, but they mostly focus on the sequential aspect of file system execution and do not comprehensively explore the concurrency dimension and hence, forgo the opportunity to catch data races.In this paper, we bring coverage-guided fuzzing to the concurrency dimension with three new constructs: 1) a new coverage tracking metric, alias coverage, specially designed to capture the exploration progress in the concurrency dimension; 2) an evolution algorithm for generating, mutating, and merging multi-threaded syscall sequences as inputs for concurrency fuzzing; and 3) a comprehensive lockset and happens-before modeling for kernel synchronization primitives for precise data race detection. These components are integrated into Krace, an end-to-end fuzzing framework that has discovered 23 data races in ext4, btrfs, and the VFS layer so far, and 9 are confirmed to be harmful.

There has been tremendous progress in the past few decades towards developing applications that receive data and send data concurrently. In such a day and age, there is a requirement for a language that can perform optimally in such environments. Currently, the two most popular languages in that respect are Go and Java. In this paper, we look to analyze the concurrency features of Go and Java through a complete programming language performance analysis, looking at their compile time, run time, binary sizes and the language's unique concurrency features. This is done by experimenting with the two languages using the matrix multiplication and PageRank algorithms. To the extent of our knowledge, this is the first work which used PageRank algorithm to analyse concurrency. Considering the results of this paper, application developers and researchers can hypothesize on an appropriate language to use for their concurrent programming activity.Results of this paper show that Go performs better for fewer number of computation but is soon taken over by Java as the number of computations drastically increase. This trend is shown to be the opposite when thread creation and management is considered where Java performs better with fewer computation but Go does better later on. Regarding concurrency features both Java with its Executor Service library and Go had their own advantages that made them better for specific applications.

Consensus protocols are currently the bottlenecks that prevent blockchain systems from scaling. However, we argue that transaction execution is also important to the performance and security of blockchains. In other words, there are ample opportunities to speed up and further secure blockchains by reducing the cost of transaction execution. Our goal is to understand how much we can speed up blockchains by exploiting transaction concurrency available in blockchain workloads. To this end, we first analyze historical data of seven major public blockchains, namely Bitcoin, Bitcoin Cash, Litecoin, Dogecoin, Ethereum, Ethereum Classic, and Zilliqa. We consider two metrics for concurrency, namely the single-transaction conflict rate per block, and the group conflict rate per block. We find that there is more concurrency in UTXO-based blockchains than in account-based ones, although the amount of concurrency in the former is lower than expected. Another interesting finding is that some blockchains with larger blocks have more concurrency than blockchains with smaller blocks. Next, we propose an analytical model for estimating the transaction execution speed-up given an amount of concurrency. Using results from our empirical analysis, the model estimates that 6× speed-ups in Ethereum can be achieved if all available concurrency is exploited.

For the last two decades, a wide spectrum of interpretations of non-interference11The notion of non-interference discussed in this paper enforces flow security in a program and is different from the concept of non-interference used for establishing functional correctness of parallel programs [1] have been used in the security analysis of programs, starting with the notion proposed by Goguen & Meseguer along with arguments of its impact on security practice. While the majority of works deal with sequential programs, several researchers have extended the notion of non-interference to enforce information flow-security in non-deterministic and concurrent programs. Major efforts of generalizations are based on (i) considering input sequences as a basic unit for input/output with semantic interpretation on a two-point information flow lattice, or (ii) typing of expressions as values for reading and writing, or (iii) typing of expressions along with its limited effects. Such approaches have limited compositionality and, thus, pose issues while extending these notions for concurrent programs. Further, in a general multi-point lattice, the notion of a public observer (or attacker) is not unique as it depends on the level of the attacker and the one attacked. In this paper, we first propose a compositional variant of non-interference for sequential systems that follow a general information flow lattice and place it in the context of earlier definitions of non-interference. We show that such an extension leads to the capturing of violations of information flow security in a concrete setting of a sequential language. Finally, we generalize non-interference for concurrent programs and illustrate its use for security analysis, particularly in the cases where information is transmitted through shared variables.

Language-based information-flow control (IFC) techniques often rely on special purpose, ad-hoc primitives to address different covert channels that originate in the runtime system, beyond the scope of language constructs. Since these piecemeal solutions may not compose securely, there is a need for a unified mechanism to control covert channels. As a first step towards this goal, we argue for the design of a general interface that allows programs to safely interact with the runtime system and the available computing resources. To coordinate the communication between programs and the runtime system, we propose the use of asynchronous exceptions (interrupts), which, to the best of our knowledge, have not been considered before in the context of IFC languages. Since asynchronous exceptions can be raised at any point during execution-often due to the occurrence of an external event-threads must temporarily mask them out when manipulating locks and shared data structures to avoid deadlocks and, therefore, breaking program invariants. Crucially, the naive combination of asynchronous exceptions with existing features of IFC languages (e.g., concurrency and synchronization variables) may open up new possibilities of information leakage. In this paper, we present MACasync, a concurrent, statically enforced IFC language that, as a novelty, features asynchronous exceptions. We show how asynchronous exceptions easily enable (out of the box) useful programming patterns like speculative execution and some degree of resource management. We prove that programs in MACasync satisfy progress-sensitive non-interference and mechanize our formal claims in the Agda proof assistant.

The Moving Picture Experts Group's Compact Descriptors for Visual Search (MPEG's CDVS) intends to standardize technologies in order to enable an interoperable, efficient, and cross-platform solution for internet-scale visual search applications and services. Among the key technologies within CDVS, we recall the format of visual descriptors, the descriptor extraction process, and the algorithms for indexing and matching. Unfortunately, these steps require precision and computation accuracy. Moreover, they are very time-consuming, as they need running times in the order of seconds when implemented on the central processing unit (CPU) of modern mobile devices. In this paper, to reduce computation times and maintain precision and accuracy, we re-design, for many-cores embedded graphical processor units (GPUs), all main local descriptor extraction pipeline phases of the MPEG's CDVS standard. To reach this goal, we introduce new techniques to adapt the standard algorithm to parallel processing. Furthermore, to reduce memory accesses and efficiently distribute the kernel workload, we use new approaches to store and retrieve CDVS information on proper GPU data structures. We present a complete experimental analysis on a large and standard test set. Our experiments show that our GPU-based approach is remarkably faster than the CPU-based reference implementation of the standard, and it maintains a comparable precision in terms of true and false positive rates.

Concurrency vulnerabilities are extremely harmful and can be frequently exploited to launch severe attacks. Due to the non-determinism of multithreaded executions, it is very difficult to detect them. Recently, data race detectors and techniques based on maximal casual model have been applied to detect concurrency vulnerabilities. However, the former are ineffective and the latter report many false negatives. In this paper, we present CONVUL, an effective tool for concurrency vulnerability detection. CONVUL is based on exchangeable events, and adopts novel algorithms to detect three major kinds of concurrency vulnerabilities. In our experiments, CONVUL detected 9 of 10 known vulnerabilities, while other tools only detected at most 2 out of these 10 vulnerabilities. The 10 vulnerabilities are available at https://github.com/mryancai/ConVul.

Cyber-event-triggered power grid blackout compels utility operators to intensify cyber-aware and physics-constrained recovery and restoration process. Recently, coordinated cyber attacks on the Ukrainian grid witnessed such a cyber-event-triggered power system blackout. Various cyber-physical system (CPS) testbeds have attempted with multitude designs to analyze such interdependent events and evaluate remedy measures. However, resource constraints and modular integration designs have been significant barriers while modeling large-scale grid models (scalability) and multi-grid isolated models (concurrency) under a single real-time execution environment for the hardware-in-the-loop (HIL) CPS security testbeds. This paper proposes a meticulous design and effective modeling for simulating large-scale grid models and multi-grid isolated models in a HIL realtime digital simulator environment integrated with industry-grade hardware and software systems. We have used our existing HIL CPS security testbed to demonstrate scalability by the realtime performance of a Texas-2000 bus US synthetic grid model and concurrency by the real-time performance of simultaneous ten IEEE-39 bus grid models and an IEEE-118 bus grid model. The experiments demonstrated significant results by 100% realtime performance with zero overruns, low latency while receiving and executing control signals from SEL Relays via IEC-61850 protocol and low latency while computing and transmitting grid data streams including stability measures via IEEE C37.118 synchrophasor data protocol to SEL Phasor Data Concentrators.

Localizing concurrency faults that occur in production is hard because, (1) detailed field data, such as user input, file content and interleaving schedule, may not be available to developers to reproduce the failure; (2) it is often impractical to assume the availability of multiple failing executions to localize the faults using existing techniques; (3) it is challenging to search for buggy locations in an application given limited runtime data; and, (4) concurrency failures at the system level often involve multiple processes or event handlers (e.g., software signals), which can not be handled by existing tools for diagnosing intra-process(thread-level) failures. To address these problems, we present SCMiner, a practical online bug diagnosis tool to help developers understand how a system-level concurrency fault happens based on the logs collected by the default system audit tools. SCMiner achieves online bug diagnosis to obviate the need for offline bug reproduction. SCMiner does not require code instrumentation on the production system or rely on the assumption of the availability of multiple failing executions. Specifically, after the system call traces are collected, SCMiner uses data mining and statistical anomaly detection techniques to identify the failure-inducing system call sequences. It then maps each abnormal sequence to specific application functions. We have conducted an empirical study on 19 real-world benchmarks. The results show that SCMiner is both effective and efficient at localizing system-level concurrency faults.

Smart contracts have been widely used on Ethereum to enable business services across various application domains. However, they are prone to different forms of security attacks due to the dynamic and non-deterministic blockchain runtime environment. In this work, we highlighted a general miner-side type of exploit, called concurrency exploit, which attacks smart contracts via generating malicious transaction sequences. Moreover, we designed a systematic algorithm to automatically detect such exploits. In our preliminary evaluation, our approach managed to identify real vulnerabilities that cannot be detected by other tools in the literature.

Use-After-Free (UAF) vulnerabilities are caused by the program operating on a dangling pointer and can be exploited to compromise critical software systems. While there have been many tools to mitigate UAF vulnerabilities, UAF remains one of the most common attack vectors. UAF is particularly di cult to detect in concurrent programs, in which a UAF may only occur with rare thread schedules. In this paper, we present a novel technique, UFO, that can precisely predict UAFs based on a single observed execution trace with a provably higher detection capability than existing techniques with no false positives. The key technical advancement of UFO is an extended maximal thread causality model that captures the largest possible set of feasible traces that can be inferred from a given multithreaded execution trace. By formulating UAF detection as a constraint solving problem atop this model, we can explore a much larger thread scheduling space than classical happens-before based techniques. We have evaluated UFO on several real-world large complex C/C++ programs including Chromium and FireFox. UFO scales to real-world systems with hundreds of millions of events in their execution and has detected a large number of real concurrency UAFs.