While existing literature on electronic voting has extensively addressed verifiability of voting protocols, the vulnerability of electoral rolls in large public elections remains a critical concern. To ensure integrity of electoral rolls, the current practice is to either make electoral rolls public or share them with the political parties. However, this enables construction of detailed voter profiles and selective targeting and manipulation of voters, thereby undermining the fundamental principle of free and fair elections. In this paper, we study the problem of designing publicly auditable yet privacy-preserving electoral rolls. We first formulate a threat model and provide formal security definitions. We then present a protocol for creation, maintenance and usage of electoral rolls that mitigates the threats. Eligible voters can verify their inclusion, whereas political parties and auditors can statistically audit the electoral roll. Further, the audit can also detect polling-day ballot stuffing and denials to eligible voters by malicious polling officers. The entire electoral roll is never revealed, which prevents any large-scale systematic voter targeting and manipulation.

We introduce the notion of traceable mixnets. In a traditional mixnet, multiple mix-servers jointly permute and decrypt a list of ciphertexts to produce a list of plaintexts, along with a proof of correctness, such that the association between individual ciphertexts and plaintexts remains completely hidden. However, in many applications, the privacy-utility tradeoff requires answering some specific queries about this association, without revealing any information beyond the query result. We consider queries of the following types: a) given a ciphertext in the mixnet input list, whether it encrypts one of a given subset of plaintexts in the output list, and b) given a plaintext in the mixnet output list, whether it is a decryption of one of a given subset of ciphertexts in the input list. Traceable mixnets allow the mix-servers to jointly prove answers to the above queries to a querier such that neither the querier nor a threshold number of mix-servers learn any information beyond the query result. Further, if the querier is not corrupted, the corrupted mix-servers do not even learn the query result. We first comprehensively formalise these security properties of traceable mixnets and then propose a construction of traceable mixnets using novel distributed zero-knowledge proofs (ZKPs) of set membership and of a statement we call reverse set membership. Although set membership has been studied in the single-prover setting, the main challenge in our distributed setting lies in making sure that none of the mix-servers learn the association between ciphertexts and plaintexts during the proof. We implement our distributed ZKPs and show that they are faster than state-of-the-art by at least one order of magnitude.

Concurrency errors due to poorly handled exceptions are common. Developers often make mistakes in writing proper code logic to relinquish the resources in the exception-handlers and cleanup blocks such as finally in Java. Our observations suggest that these mistakes often go unnoticed because the exception-handling code is generally not tested in the development phase. These errors materialize when the exception handlers execute within the production environment. Therefore, verifying multi-threaded programs augmented with their exception handlers is necessary to guarantee their correctness. This paper proposes a dynamic technique to verify exception-handling code in concurrent libraries. The technique detects the presence of deadlocks originating from exception-handling code. We also present a prototype called Lumina,that implements our technique to demonstrate that it can detect the deadlocks effectively, unlike the state-of-the-art dynamic verifier JavaPathfinder (JPF).

The generation of adversarial inputs has become a crucial issue in establishing the robustness and trustworthiness of deep neural nets, especially when they are used in safety-critical application domains such as autonomous vehicles and precision medicine. However, the problem poses multiple practical challenges, including scalability issues owing to large-sized networks, and the generation of adversarial inputs that lack important qualities such as naturalness and output-impartiality. This problem shares its end goal with the task of patching neural nets where small changes in some of the network’s weights need to be discovered so that upon applying these changes, the modified net produces the desirable output for a given set of inputs. We exploit this connection by proposing to obtain an adversarial input from a patch, with the underlying observation that the effect of changing the weights can also be brought about by changing the inputs instead. Thus, this paper presents a novel way to generate input perturbations that are adversarial for a given network by using an efficient network patching technique. We note that the proposed method is significantly more effective than the prior state-of-the-art techniques.

Communication nondeterminism is one of the main reasons for the intractability of verification of message passing concurrency. In many practical message passing programs, the non-deterministic communication structure is symmetric and decomposed into epochs to obtain efficiency. Thus, symmetries and epoch structure can be exploited to reduce verification complexity. In this paper, we present a dynamic-symbolic runtime verification technique for single-path MPI programs, which (i) exploits communication symmetries by way of specifying symmetry breaking predicates (SBP) and (ii) performs compositional verification based on epochs. On the one hand, SBPs prevent the symbolic decision procedure from exploring isomorphic parts of the search space, and on the other hand, epochs restrict the size of a program needed to be analyzed at a point in time. We show that our analysis is sound and complete for single-path MPI programs on a given input. Using our prototype tool SIMIAN, we further demonstrate that our approach leads to (i) a significant reduction in verification times and (ii) scaling up to larger benchmark sizes compared to prior trace verifiers.

Instruction reordering and interleavings in program execution under relaxed memory semantics result in non-intuitive behaviors, making it difficult to provide assurances about program correctness. Studies have shown that up to 90% of the concurrency bugs reported by state-of-the-art static analyzers are false alarms. As a result, filtering false alarms and detecting real concurrency bugs is a challenging problem. Unsurprisingly, this problem has attracted the interest of the research community over the past few decades. Nonetheless, many of the existing techniques rely on analyzing source code, rarely consider the effects introduced by compilers, and assume a sequentially consistent memory model. In a practical setting, however, developers often do not have access to the source code, and even commodity architectures such as x86 and ARM are not sequentially consistent. In this work, we present B i rd , a prototype tool, to dynamically detect harmful data races in x86 binaries under relaxed memory models, TSO and PSO. B i rd employs source-DPOR to explore all distinct feasible interleavings for a multithreaded application. Our evaluation of B i rd on 42 publicly available benchmarks and its comparison with the state-of-the-art tools indicate B i rd ’s potential in effectively detecting data races in software binaries.

Multi-threaded libraries, including the ones advertised as thread-safe, may contain concurrency bugs, and worse, may not include relevant test cases that can drive the program execution towards bug-prone interleavings. Also, the effectiveness of dynamic verification, a prominent concurrency bug detection technique, depends critically on the availability of relevant test cases. Generating such test cases automatically to assist dynamic verification is, therefore, a significant problem.Among hard-to-detect concurrency bugs in multi-threaded Java libraries are communication deadlocks, which occur due to the incorrect usage of wait() and notify() communication primitives. In this work, we present a novel technique to systematically synthesize multi-threaded test cases to expose communication deadlocks. We model these deadlocks as global constraints over the events of two sequential program traces of the library APIs. The task of predicting the relevance of combining two sequential program traces is delegated to an SMT solver. We implement our technique in a prototype tool named REVELIO, and evaluate it on fifteen classes of popular multi-threaded Java libraries. We find that REVELIO is able to synthesize precise tests exposing communication deadlocks, which the state-of-the-art tools cannot.

We investigate the problem of runtime analysis of concurrent C11 programs under Multi-Copy-Atomic semantics (MCA). Under MCA, one can analyze program outcomes solely through interleaving and reordering of thread events. As a result, obtaining intuitive explanations of program outcomes becomes straightforward. Newer versions of ARM (ARMv8 and later), Alpha, and Intel’s x-86 support MCA. Our tests reveal that state-of-the-art dynamic verification techniques that analyze program executions under the C11 memory model report safety property violations that can be interpreted as false alarms under MCA semantics. Sorting the true from false violations puts an undesirable burden on the user.In this work, we provide a dynamic verification technique (MoCA) to analyze C11 program executions which are permitted under the MCA model. We restrict C11 happens-before relation and propose coherence rules to capture precisely those C11 program executions which are allowed under the MCA model. MoCA’s exploration of the state-space is based on the state-of-the-art dynamic verification algorithm, source-DPOR. Our experiments validate that MoCA captures all coherent C11 program executions, and is precise for the MCA model.

The success of dynamic verification techniques for confirming the absence of bugs in concurrent programs rests on their ability to systematically address the interleaving space arising because of the nondeterminism. However, existing dynamic verification engines suffer from the problem of scalability due to the size of the reachable state space that grows exponentially as the number of parallel entities increases. The second front on which the dynamic verification technique struggles is the dependence on the test cases to drive the program, thus being as efficient as the quality of the test cases. Lastly, any verification technique suffers from the lack of a significant benchmark of bugs to prove its worth. This work tries to improve the area of dynamic verification concerning the limitations as mentioned above. We utilize the worthiness and popularity of constraint solvers and establish our work in the realm of concurrent programs.

Synchronous reactive data flow is a paradigm that provides a high-level abstract programming model for embedded and cyber-physical systems, including the locally synchronous components of IoT systems. Security in such systems is severely compromised due to low-level programming, ill-defined interfaces and inattention to security classification of data. By incorporating a Denning-style lattice-based secure information flow framework into a synchronous reactive data flow language, we provide a framework in which correct-and-secure-by-construction implementations for such systems can be specified and derived. In particular, we propose an extension of the Lustre programming framework with a security type system. We prove the soundness of our type system with respect to the co-inductive operational semantics of Lustre by showing that well-typed programs exhibit non-interference.

The Message Passing Interface (MPI) is the standard API for parallelization in high-performance and scientific computing. Communication deadlocks are a frequent problem in MPI programs, and this article addresses the problem of discovering such deadlocks. We begin by showing that if an MPI program is single path, the problem of discovering communication deadlocks is NP-complete. We then present a novel propositional encoding scheme that captures the existence of communication deadlocks. The encoding is based on modeling executions with partial orders and implemented in a tool called MOPPER . The tool executes an MPI program, collects the trace, builds a formula from the trace using the propositional encoding scheme, and checks its satisfiability. Finally, we present experimental results that quantify the benefit of the approach in comparison to other analyzers and demonstrate that it offers a scalable solution for single-path programs.

Software evolution in third-party libraries across version upgrades can result in addition of new functionalities or change in existing APIs. As a result, there is a real danger of impairment of backward compatibility. Application developers, therefore, must keep constant vigil over library enhancements to ensure application consistency, i.e., application retains its semantic behavior across library upgrades. In this paper, we present the design and implementation of POLLUX, a framework to detect application-affecting changes across two versions of the same dependent non-adversarial library binary, and provide feedback on whether the application developer should link to the newer version or not. POLLUX leverages relevant application test cases to drive execution through both versions of the concerned library binary, records all concrete effects on the environment, and compares them to determine semantic similarity across the same API invocation for the two library versions. Our evaluation with 16 popular, open-source library binaries shows that POLLUX is accurate with no false positives and works across compiler optimizations.

Nondeterminism in scheduling is the cardinal reason for difficulty in proving correctness of concurrent programs. A powerful proof strategy was recently proposed [6] to show the correctness of such programs. The approach captured data-flow dependencies among the instructions of an interleaved and error-free execution of threads. These data-flow dependencies were represented by an inductive data-flow graph (iDFG), which, in a nutshell, denotes a set of executions of the concurrent program that gave rise to the discovered data-flow dependencies. The iDFGs were further transformed in to alternative finite automatons (AFAs) in order to utilize efficient automata-theoretic tools to solve the problem. In this paper, we give a novel and efficient algorithm to directly construct AFAs that capture the data-flow dependencies in a concurrent program execution. We implemented the algorithm in a tool called ProofTraPar to prove the correctness of finite state cyclic programs under the sequentially consistent memory model. Our results are encouraging and compare favorably to existing state-of-the-art tools.

Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to combine their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a novel stateless POR algorithm that explores at most one execution per Mazurkiewicz trace, and in general, can explore exponentially fewer, thus achieving a form of super-optimality. Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state caching. On benchmarks with busy-waits, among others, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR.

As product life-cycles become shorter and the scale and complexity of systems increase, accelerating the execution of large test suites gains importance. Existing research has primarily focussed on techniques that reduce the size of the test suite. By contrast, we propose a technique that accelerates test execution, allowing test suites to run in a fraction of the original time, by parallel execution with a Graphics Processing Unit (GPU).

We present a dynamic verification tool MCC for Multicore Communication API applications - a new API for communication among cores. MCC systematically explores all relevant interleavings of an MCAPI application using a tailor-made dynamic partial order reduction algorithm (DPOR). Our contributions are (i) a way to model the non-overtaking message matching relation underlying MCAPI calls with a high level algorithm to effect DPOR for MCAPI that controls the lower level details so that the intended executions happen at runtime; and (ii) a list of default safety properties that can be utilized in the process of verification. To our knowledge, this is the first push button model checker for MCAPI application writers that, at present, deals with an interesting subset of MCAPI calls. Our result is the demonstration that we can indeed develop a dynamic model checker for MCAPI that can directly control the non-deterministic behavior at runtime that is inherent in any implementation of the library without additional API modifications or additions.

No abstract available.