BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Subodh Sharma

Subodh Sharma appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Programming LanguagesLogic in Computer ScienceDistributed, Parallel, and Cluster ComputingCryptography and Securitycs.CYSoftware Engineering

Catalog footprint

What is connected

8works
6topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

8 published item(s)

preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

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.

0 citations0 reviewsNo code linkedOpen access