arXiv subjects

Subodh Sharma

Publications and source records attributed to Subodh Sharma.

16 recordsLinked to original sources

arXiv2025

BugMagnifier: TON Transaction Simulator for Revealing Smart Contract Vulnerabilities

The Open Network (TON) blockchain employs an asynchronous execution model that introduces unique security challenges for smart contracts. A primary concern is race conditions arising from unpredictable message processing order. While previous work established vulnerability patterns through static analysis of audit reports, dynamic detection of temporal dependencies through systematic testing remains an open problem. This study proposes a dynamic evaluation methodology based on controlled message orchestration to systematically expose vulnerabilities in asynchronous smart contracts. By synthesizing precise message queue manipulation with differential state analysis and probabilistic permutation testing, we establish a framework (namely, BugMagnifier) for identifying execution flaws that static methods miss. Experimental evaluation demonstrates BugMagnifier's effectiveness through extensive parametric studies on purpose-built vulnerable contracts and five real-world vulnerability cases reproduced from recent security audits. Results reveal message ratio-dependent detection complexity that aligns with theoretical predictions. This quantitative model enables predictive vulnerability assessment while shifting discovery from manual expert analysis to automated evidence generation. By providing reproducible test scenarios for temporal vulnerabilities, BugMagnifier addresses a critical gap in the TON security tooling, offering practical support for safer smart contract development in asynchronous blockchain environments.

cs.CR↗

arXiv2025

From Paradigm Shift to Audit Rift: Empirical Analysis and Validation of Security Audit Methodologies for Asynchronous Smart Contract Systems

The Open Network (TON) is a high-performance blockchain platform designed for scalability and efficiency, leveraging an asynchronous execution model and a multi-layered architecture. While TON's design offers significant advantages, it also introduces unique challenges for smart contract development and security. This paper introduces a comprehensive audit checklist for TON smart contracts, based on an empirical analysis of 34 professional audit reports containing 233 real-world vulnerabilities. The checklist addresses TON-specific challenges, such as asynchronous message handling, and provides actionable insights for developers and auditors. We also present detailed case studies of vulnerabilities in TON smart contracts, highlighting their implications and offering lessons learned. To validate practical utility, we conducted a practitioner survey (n=11 complete responses), confirming the checklist's value alongside automated tools. By adopting this checklist, developers and auditors can systematically identify and mitigate vulnerabilities, enhancing the security and reliability of TON-based projects. Our work bridges the gap between Ethereum's mature audit methodologies and the emerging needs of the TON ecosystem, fostering a more secure and robust blockchain environment.

cs.CR↗

arXiv2023

Symbolic Security Verification of Mesh Commissioning Protocol in Thread (extended version)

The Thread protocol (or simply Thread ) is a popular networking protocol for the Internet of Things (IoT). It allows seamless integration of a set of applications and protocols, hence reducing the risk of incompatibility among different applications or user protocols. Thread has been deployed in many popular smart home products by the majority of IoT manufacturers, such as Apple TV, Apple HomePod mini, eero 6, Nest Hub, and Nest Wifi. Despite a few empirical analyses on the security of Thread, there is still a lack of formal analysis on this infrastructure of the booming IoT ecosystem. In this work, we performed a formal symbolic analysis of the security properties of Thread. Our main focus is on MeshCoP (Mesh Commissioning Protocol), the main subprotocol in Thread for secure authentication and commissioning of new, untrusted devices inside an existing Thread network. This case study presents the challenges and proposed solutions in modeling MeshCoP. We use ProVerif, a symbolic verification tool of {\pi}-calculus models, for verifying the security properties of MeshCoP.

cs.CR↗

arXiv2023

Ballot stuffing and participation privacy in pollsite voting

We study the problem of simultaneously addressing both ballot stuffing and participation privacy for pollsite voting systems. Ballot stuffing is the attack where fake ballots (not cast by any eligible voter) are inserted into the system. Participation privacy is about hiding which eligible voters have actually cast their vote. So far, the combination of ballot stuffing and participation privacy has been mostly studied for internet voting, where voters are assumed to own trusted computing devices. Such approaches are inapplicable to pollsite voting where voters typically vote bare handed. We present an eligibility audit protocol to detect ballot stuffing in pollsite voting protocols. This is done while protecting participation privacy from a remote observer - one who does not physically observe voters during voting. Our protocol can be instantiated as an additional layer on top of most existing pollsite E2E-V voting protocols. To achieve our guarantees, we develop an efficient zero-knowledge proof (ZKP), that, given a value $v$ and a set $Φ$ of commitments, proves $v$ is committed by some commitment in $Φ$, without revealing which one. We call this a ZKP of reverse set membership because of its relationship to the popular ZKPs of set membership. This ZKP may be of independent interest.

cs.CR↗

arXiv2023

Traceable mixnets

We introduce the notion of \emph{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.

cs.CR↗

arXiv2022

Fence Synthesis under the C11 Memory Model

The C/C++11 (C11) standard offers a spectrum of ordering guarantees on memory access operations. The combinations of such orderings pose a challenge in developing correct and efficient weak memory programs. A common solution to preclude those program outcomes that violate the correctness specification is using C11 synchronization-fences, which establish ordering on program events. The challenge is in choosing a combination of fences that (i) restores the correctness of the input program, with (ii) as little impact on efficiency as possible (i.e., the smallest set of weakest fences). This problem is the optimal fence synthesis problem and is NP-hard for straight-line programs. In this work, we propose the first fence synthesis technique for C11 programs called FenSying and show its optimality. We additionally propose a near-optimal efficient alternative called fFenSying. We prove the optimality of FenSying and the soundness of fFenSying and present an implementation of both techniques. Finally, we contrast the performance of the two techniques and empirically demonstrate fFenSyings effectiveness.

cs.DC↗

arXiv2022

Dynamic Verification with Observational Equivalence of C/C++ Concurrency

Program executions under relaxed memory model (rmm) semantics are significantly more difficult to analyze; the rmm semantics result in out of order execution of program events leading to an explosion of state-space. Dynamic partial order reduction (DPOR) is a powerful technique to address such a state-space explosion and has been used to verify programs under rmm such as TSO, PSO, and POWER. Central to such DPOR techniques is the notion of trace-equivalence, which is computed based on the independence relation among program events. We propose a coarser notion of rmm-aware trace equivalence called observational equivalence (OE). Two program behaviors are observationally equivalent if every read event reads the same value in both the behaviors. We propose a notion of observational independence (OI) and provide an algorithmic construction to compute trace equivalence (modulo OI) efficiently. We also demonstrate the effectiveness of DPOR with OE on threaded C/C++ programs by first providing an elaborate happensbefore (hb) relation for capturing the C/C++ concurrency semantics. We implement the presented technique in a runtime model checker called Drista. Our experiments reflect that (i) when compared to existing nonOE techniques, we achieve significant savings in the number of traces explored under OE, and (ii) our treatment of C/C++ concurrency is more extensive than the existing state-of-the-art techniques.

cs.PL↗

arXiv2022

Secure Information Flow Typing in LUSTRE

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 may be specified and derived. In particular, we propose an extension of the Lustre programming framework with a security type system. The novelty of our type system lies in a symbolic formulation of constraints over security type variables, in particular the treatment of node calls, which allows us to reason about secure flow with respect to any security class lattice. The main theorem is the soundness of our type system with respect to the co-inductive operational semantics of Lustre, which we prove by showing that well-typed programs exhibit non-interference. Rather than tackle the full language, we first prove the non-interference result for a well-behaved sub-language called "Normalised Lustre" (NLustre), for which our type system is far simpler. We then show that Bourke et al.'s semantics-preserving "normalisation" transformations from Lustre to NLustre are security-preserving as well. This preservation of security types by the normalisation transformations is a property akin to "subject reduction" but at the level of compiler transformations. The main result that well-security-typed Lustre programs are non-interfering follows from a reduction to our earlier result of non-interference for NLustre via the semantics-preservation (of Bourke et al.) and type preservation results.

cs.PL↗

arXiv2021

Thread-modular Analysis of Release-Acquire Concurrency

We present a thread-modular abstract interpretation(TMAI) technique to verify programs under the release-acquire (RA) memory model for safety property violations. The main contributions of our work are: we capture the execution order of program statements as an abstract domain, and propose a sound upper approximation over this domain to efficiently reason over RA concurrency. The proposed domain is general in its application and captures the ordering relations as a first-class feature in the abstract interpretation theory. In particular, the domain represents a set of sequences of modifications of a global variable in concurrent programs as a partially ordered set. Under this approximation, older sequenced-before stores of a global variable are forgotten and only the latest stores per variable are preserved. We establish the soundness of our proposed abstractions and implement them in a prototype abstract interpreter called PRIORI. The evaluations of PRIORI on existing and challenging RA benchmarks demonstrate that the proposed technique is not only competitive in refutation, but also in verification. PRIORI shows significantly fast analysis runtimes with higher precision compared to recent state-of-the-art tools for RA concurrency.

cs.PL↗

arXiv2021

Dynamic Verification of C/C++11 Concurrency over Multi Copy Atomics

We investigate the problem of runtime analysis of 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 generate 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 design a happens-before relation and introduce 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.

cs.PL↗

arXiv2020

An operational architecture for privacy-by-design in public service applications

Governments around the world are trying to build large data registries for effective delivery of a variety of public services. However, these efforts are often undermined due to serious concerns over privacy risks associated with collection and processing of personally identifiable information. While a rich set of special-purpose privacy-preserving techniques exist in computer science, they are unable to provide end-to-end protection in alignment with legal principles in the absence of an overarching operational architecture to ensure purpose limitation and protection against insider attacks. This either leads to weak privacy protection in large designs, or adoption of overly defensive strategies to protect privacy by compromising on utility. In this paper, we present an operational architecture for privacy-by-design based on independent regulatory oversight stipulated by most data protection regimes, regulated access control, purpose limitation and data minimisation. We briefly discuss the feasibility of implementing our architecture based on existing techniques. We also present some sample case studies of privacy-preserving design sketches of challenging public service applications.

cs.CR↗

arXiv2019

OpenVoting: Recoverability from Failures in Dual Voting

In this paper we address the problem of recovery from failures without re-running entire elections when elections fail to verify. We consider the setting of \emph{dual voting} protocols, where the cryptographic guarantees of end-to-end verifiable voting (E2E-V) are combined with the simplicity of audit using voter-verified paper records (VVPR). We first consider the design requirements of such a system and then suggest a protocol called \emph{OpenVoting}, which identifies a verifiable subset of error-free votes consistent with the VVPRs, and the polling booths corresponding to the votes that fail to verify with possible reasons for the failures. To an ordinary voter \emph{OpenVoting} looks just like an old fashioned paper based voting system, with minimal additional cognitive overload.

cs.CR↗

arXiv2016

Efficient Verification of Concurrent Programs Over TSO Memory Model

We address the problem of efficient verification of multi-threaded programs running over Total Store Order (TSO) memory model. It has been shown that even with finite data domain programs, the complexity of control state reachability under TSO is non-primitive recursive. In this paper, we first present a bounded-buffer verification approach wherein a bound on the size of buffers is placed; verification is performed incrementally by increasing the size of the buffer with each iteration of the verification procedure until the said bound is reached. For programs operating on finite data domains, we also demonstrate the existence of a buffer bound k such that if the program is safe under that bound, then it is also safe for unbounded buffers. We have implemented this technique in a tool ProofTraPar. Our results against memorax [2], a state-of-the-art sound and complete verifier for TSO memory model, have been encouraging.

cs.LO↗

arXiv2016

From Traces To Proofs: Proving Concurrent Program Safe

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 encouranging and compare favorably to existing state-of-the-art tools.

cs.PL↗

arXiv2015

Unfolding-based Partial Order Reduction

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. Over 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.

cs.LO↗

arXiv2014

AbPress: Flexing Partial-Order Reduction and Abstraction

Partial-order reduction (POR) and lazy abstraction with interpolants are two complementary techniques that have been successfully employed to make model checking tools for concurrent programs effective. In this work, we present AbPress - Abstraction-based Partial-order Reduction with Source-Sets - an algorithm that fuses a recently proposed and powerful dynamic POR technique based on source-sets and lazy abstraction to obtain an efficient software model checker for multi-threaded programs. It trims the inter- leaving space by taking the abstraction and source-sets into account. We amplify the effectiveness of AbPress with a novel solution that summarizes the accesses to shared variables over a collection of interleavings. We have implemented AbPress in a tool that analyzes concurrent programs using lazy abstraction, viz., Impara. Our evaluation on the effectiveness of the presented approach has been encouraging. AbPress compares favorably to existing state-of-the-art tools in the landscape.

cs.LO↗