8 citations · 15 across the 13 of their papers we have counts for
14 papers
From Paradigm Shift to Audit Rift: Empirical Analysis and Validation of Security Audit Methodologies for Asynchronous Smart Contract Systems
Yury Yanovich, Sergey Sobolev, Yash Madhwal +6
The Open Network (TON) is a high-performance blockchain platform designed for scalability and efficiency, leveraging an asynchronous execution model and a multi-layered architectur…
Traceable mixnets
Prashant Agrawal, Abhinav Nakarmi, Mahavir Prasad Jhawar +2
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…
Ballot stuffing and participation privacy in pollsite voting
Prashant Agrawal, Abhinav Nakarmi, Mahabir Prasad Jhanwar +2
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…
Fence Synthesis under the C11 Memory Model
Sanjana Singh, Divyanjali Sharma, Ishita Jaju +1
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 effic…
Secure Information Flow Typing in LUSTRE
Sanjiva Prasad, R. Madhukar Yerraguntla, Subodh Sharma
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 compon…
Thread-modular Analysis of Release-Acquire Concurrency
Divyanjali Sharma, Subodh Sharma
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 contribu…
Dynamic Verification of C/C++11 Concurrency over Multi Copy Atomics
Sanjana Singh, Divyanjali Sharma, Subodh Sharma
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…
An operational architecture for privacy-by-design in public service applications
Prashant Agrawal, Anubhutie Singh, Malavika Raghavan +2
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 se…
OpenVoting: Recoverability from Failures in Dual Voting
Prashant Agrawal, Kabir Tomer, Abhinav Nakarmi +3
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} prot…
Dynamic Verification with Observational Equivalence of C/C++ Concurrency
Sanjana Singh, Divyanjali Sharma, Subodh Sharma
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 lead…
Efficient Verification of Concurrent Programs Over TSO Memory Model
Chinmay Narayan, Subodh Sharma, S. Arun-Kumar
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 p…
Unfolding-based Partial Order Reduction
César Rodríguez, Marcelo Sousa, Subodh Sharma +1
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 bot…
From Traces To Proofs: Proving Concurrent Program Safe
Chinmay Narayan, Subodh Sharma, Shibashis Guha +1
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 co…
AbPress: Flexing Partial-Order Reduction and Abstraction
Daniel Kroening, Subodh Sharma, Björn Wachter
Partial-order reduction (POR) and lazy abstraction with interpolants are two complementary techniques that have been successfully employed to make model checking tools for concurre…