Showing 1–26 of 26 results for author: Lal, A

Bridging Model-Based Optimization and Generative Modeling via Conservative Fine-Tuning of Diffusion Models

Authors: Masatoshi Uehara, Yulai Zhao, Ehsan Hajiramezanali, Gabriele Scalia, Gökcen Eraslan, Avantika Lal, Sergey Levine, Tommaso Biancalani

Abstract: AI-driven design problems, such as DNA/protein sequence design, are commonly tackled from two angles: generative modeling, which efficiently captures the feasible design space (e.g., natural images or biological sequences), and model-based optimization, which utilizes reward models for extrapolation. To combine the strengths of both approaches, we adopt a hybrid method that fine-tunes cutting-edge… ▽ More AI-driven design problems, such as DNA/protein sequence design, are commonly tackled from two angles: generative modeling, which efficiently captures the feasible design space (e.g., natural images or biological sequences), and model-based optimization, which utilizes reward models for extrapolation. To combine the strengths of both approaches, we adopt a hybrid method that fine-tunes cutting-edge diffusion models by optimizing reward models through RL. Although prior work has explored similar avenues, they primarily focus on scenarios where accurate reward models are accessible. In contrast, we concentrate on an offline setting where a reward model is unknown, and we must learn from static offline datasets, a common scenario in scientific domains. In offline scenarios, existing approaches tend to suffer from overoptimization, as they may be misled by the reward model in out-of-distribution regions. To address this, we introduce a conservative fine-tuning approach, BRAID, by optimizing a conservative reward model, which includes additional penalization outside of offline data distributions. Through empirical and theoretical analysis, we demonstrate the capability of our approach to outperform the best designs in offline data, leveraging the extrapolation capabilities of reward models while avoiding the generation of invalid designs through pre-trained diffusion models. △ Less

Submitted 31 May, 2024; v1 submitted 29 May, 2024; originally announced May 2024.

Comments: Under review

Enabling Memory Safety of C Programs using LLMs

Authors: Nausheen Mohammed, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma

Abstract: Memory safety violations in low-level code, written in languages like C, continues to remain one of the major sources of software vulnerabilities. One method of removing such violations by construction is to port C code to a safe C dialect. Such dialects rely on programmer-supplied annotations to guarantee safety with minimal runtime overhead. This porting, however, is a manual process that impose… ▽ More Memory safety violations in low-level code, written in languages like C, continues to remain one of the major sources of software vulnerabilities. One method of removing such violations by construction is to port C code to a safe C dialect. Such dialects rely on programmer-supplied annotations to guarantee safety with minimal runtime overhead. This porting, however, is a manual process that imposes significant burden on the programmer and, hence, there has been limited adoption of this technique. The task of porting not only requires inferring annotations, but may also need refactoring/rewriting of the code to make it amenable to such annotations. In this paper, we use Large Language Models (LLMs) towards addressing both these concerns. We show how to harness LLM capabilities to do complex code reasoning as well as rewriting of large codebases. We also present a novel framework for whole-program transformations that leverages lightweight static analysis to break the transformation into smaller steps that can be carried out effectively by an LLM. We implement our ideas in a tool called MSA that targets the CheckedC dialect. We evaluate MSA on several micro-benchmarks, as well as real-world code ranging up to 20K lines of code. We showcase superior performance compared to a vanilla LLM baseline, as well as demonstrate improvement over a state-of-the-art symbolic (non-LLM) technique. △ Less

Submitted 1 April, 2024; originally announced April 2024.

Resource Leak Checker (RLC#) for C# Code using CodeQL

Authors: Pritam Gharat, Narges Shadab, Shrey Tiwari, Shuvendu Lahiri, Akash Lal

Abstract: Resource leaks occur when a program fails to release a finite resource after it is no longer needed. These leaks are a significant cause of real-world crashes and performance issues. Given their critical impact on software performance and security, detecting and preventing resource leaks is a crucial problem. Recent research has proposed a specify-and-check approach to prevent resource leaks. In… ▽ More Resource leaks occur when a program fails to release a finite resource after it is no longer needed. These leaks are a significant cause of real-world crashes and performance issues. Given their critical impact on software performance and security, detecting and preventing resource leaks is a crucial problem. Recent research has proposed a specify-and-check approach to prevent resource leaks. In this approach, programmers write resource management specifications that guide how resources are stored, passed around, and released within an application. We have developed a tool called RLC#, for detecting resource leaks in C# code. Inspired by the Resource Leak Checker (RLC) from the Checker Framework, RLC# employs CodeQL for intraprocedural data flow analysis. The tool operates in a modular fashion and relies on resource management specifications integrated at method boundaries for interprocedural analysis. In practice, RLC# has successfully identified 24 resource leaks in open-source projects and internal proprietary Azure microservices. Its implementation is declarative, and it scales well. While it incurs a reasonable false positive rate, the burden on developers is minimal, involving the addition of specifications to the source code. △ Less

Submitted 5 December, 2023; v1 submitted 4 December, 2023; originally announced December 2023.

Finding Inductive Loop Invariants using Large Language Models

Authors: Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma

Abstract: Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting t… ▽ More Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification. △ Less

Submitted 14 November, 2023; originally announced November 2023.

On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability

Authors: Shankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis, Omkar Tuppe

Abstract: Dyck reachability is a principled, graph-based formulation of a plethora of static analyses. Bidirected graphs are used for capturing dataflow through mutable heap data, and are usual formalisms of demand-driven points-to and alias analyses. The best (offline) algorithm runs in $O(m+n\cdot α(n))$ time, where $n$ is the number of nodes and $m$ is the number of edges in the flow graph, which becomes… ▽ More Dyck reachability is a principled, graph-based formulation of a plethora of static analyses. Bidirected graphs are used for capturing dataflow through mutable heap data, and are usual formalisms of demand-driven points-to and alias analyses. The best (offline) algorithm runs in $O(m+n\cdot α(n))$ time, where $n$ is the number of nodes and $m$ is the number of edges in the flow graph, which becomes $O(n^2)$ in the worst case. In the everyday practice of program analysis, the analyzed code is subject to continuous change, with source code being added and removed. On-the-fly static analysis under such continuous updates gives rise to dynamic Dyck reachability, where reachability queries run on a dynamically changing graph, following program updates. Naturally, executing the offline algorithm in this online setting is inadequate, as the time required to process a single update is prohibitively large. In this work we develop a novel dynamic algorithm for bidirected Dyck reachability that has $O(n\cdot α(n))$ worst-case performance per update, thus beating the $O(n^2)$ bound, and is also optimal in certain settings. We also implement our algorithm and evaluate its performance on on-the-fly data-dependence and alias analyses, and compare it with two best known alternatives, namely (i) the optimal offline algorithm, and (ii) a fully dynamic Datalog solver. Our experiments show that our dynamic algorithm is consistently, and by far, the top performing algorithm, exhibiting speedups in the order of 1000X. The running time of each update is almost always unnoticeable to the human eye, making it ideal for the on-the-fly analysis setting. △ Less

Submitted 7 November, 2023; originally announced November 2023.

Ranking LLM-Generated Loop Invariants for Program Verification

Authors: Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury, Madanlal Musuvathi, Akash Lal, Aseem Rastogi, Aditya Senthilnathan, Rahul Sharma, Nikhil Swamy

Abstract: Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an… ▽ More Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable of synthesizing loop invariants for a class of programs in a 0-shot setting, yet require several samples to generate the correct invariants. This can lead to a large number of calls to a program verifier to establish an invariant. To address this issue, we propose a {\it re-ranking} approach for the generated results of LLMs. We have designed a ranker that can distinguish between correct inductive invariants and incorrect attempts based on the problem definition. The ranker is optimized as a contrastive ranker. Experimental results demonstrate that this re-ranking mechanism significantly improves the ranking of correct invariants among the generated candidates, leading to a notable reduction in the number of calls to a verifier. The source code and the experimental data for this paper are available in \url{https://github.com/microsoft/NeuralInvariantRanker}. △ Less

Submitted 12 February, 2024; v1 submitted 13 October, 2023; originally announced October 2023.

Comments: Findings of The 2023 Conference on Empirical Methods in Natural Language Processing (EMNLP-findings 2023)

Fixing Rust Compilation Errors using LLMs

Authors: Pantazis Deligiannis, Akash Lal, Nikita Mehrotra, Aseem Rastogi

Abstract: The Rust programming language, with its safety guarantees, has established itself as a viable choice for low-level systems programming language over the traditional, unsafe alternatives like C/C++. These guarantees come from a strong ownership-based type system, as well as primitive support for features like closures, pattern matching, etc., that make the code more concise and amenable to reasonin… ▽ More The Rust programming language, with its safety guarantees, has established itself as a viable choice for low-level systems programming language over the traditional, unsafe alternatives like C/C++. These guarantees come from a strong ownership-based type system, as well as primitive support for features like closures, pattern matching, etc., that make the code more concise and amenable to reasoning. These unique Rust features also pose a steep learning curve for programmers. This paper presents a tool called RustAssistant that leverages the emergent capabilities of Large Language Models (LLMs) to automatically suggest fixes for Rust compilation errors. RustAssistant uses a careful combination of prompting techniques as well as iteration with an LLM to deliver high accuracy of fixes. RustAssistant is able to achieve an impressive peak accuracy of roughly 74% on real-world compilation errors in popular open-source Rust repositories. We plan to release our dataset of Rust compilation errors to enable further research. △ Less

Submitted 9 August, 2023; originally announced August 2023.

Inference of Resource Management Specifications

Authors: Narges Shadab, Pritam Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu Lahiri, Akash Lal, Manu Sridharan

Abstract: A resource leak occurs when a program fails to free some finite resource after it is no longer needed. Such leaks are a significant cause of real-world crashes and performance problems. Recent work proposed an approach to prevent resource leaks based on checking resource management specifications. A resource management specification expresses how the program allocates resources, passes them around… ▽ More A resource leak occurs when a program fails to free some finite resource after it is no longer needed. Such leaks are a significant cause of real-world crashes and performance problems. Recent work proposed an approach to prevent resource leaks based on checking resource management specifications. A resource management specification expresses how the program allocates resources, passes them around, and releases them; it also tracks the ownership relationship between objects and resources, and aliasing relationships between objects. While this specify-and-verify approach has several advantages compared to prior techniques, the need to manually write annotations presents a significant barrier to its practical adoption. This paper presents a novel technique to automatically infer a resource management specification for a program, broadening the applicability of specify-and-check verification for resource leaks. Inference in this domain is challenging because resource management specifications differ significantly in nature from the types that most inference techniques target. Further, for practical effectiveness, we desire a technique that can infer the resource management specification intended by the developer, even in cases when the code does not fully adhere to that specification. We address these challenges through a set of inference rules carefully designed to capture real-world coding patterns, yielding an effective fixed-point-based inference algorithm. We have implemented our inference algorithm in two different systems, targeting programs written in Java and C#. In an experimental evaluation, our technique inferred 85.5% of the annotations that programmers had written manually for the benchmarks. Further, the verifier issued nearly the same rate of false alarms with the manually-written and automatically-inferred annotations. △ Less

Submitted 21 September, 2023; v1 submitted 20 June, 2023; originally announced June 2023.

EDoG: Adversarial Edge Detection For Graph Neural Networks

Authors: Xiaojun Xu, Yue Yu, Hanzhang Wang, Alok Lal, Carl A. Gunter, Bo Li

Abstract: Graph Neural Networks (GNNs) have been widely applied to different tasks such as bioinformatics, drug design, and social networks. However, recent studies have shown that GNNs are vulnerable to adversarial attacks which aim to mislead the node or subgraph classification prediction by adding subtle perturbations. Detecting these attacks is challenging due to the small magnitude of perturbation and… ▽ More Graph Neural Networks (GNNs) have been widely applied to different tasks such as bioinformatics, drug design, and social networks. However, recent studies have shown that GNNs are vulnerable to adversarial attacks which aim to mislead the node or subgraph classification prediction by adding subtle perturbations. Detecting these attacks is challenging due to the small magnitude of perturbation and the discrete nature of graph data. In this paper, we propose a general adversarial edge detection pipeline EDoG without requiring knowledge of the attack strategies based on graph generation. Specifically, we propose a novel graph generation approach combined with link prediction to detect suspicious adversarial edges. To effectively train the graph generative model, we sample several sub-graphs from the given graph data. We show that since the number of adversarial edges is usually low in practice, with low probability the sampled sub-graphs will contain adversarial edges based on the union bound. In addition, considering the strong attacks which perturb a large number of edges, we propose a set of novel features to perform outlier detection as the preprocessing for our detection. Extensive experimental results on three real-world graph datasets including a private transaction rule dataset from a major company and two types of synthetic graphs with controlled properties show that EDoG can achieve above 0.8 AUC against four state-of-the-art unseen attack strategies without requiring any knowledge about the attack type; and around 0.85 with knowledge of the attack type. EDoG significantly outperforms traditional malicious edge detection baselines. We also show that an adaptive attack with full knowledge of our detection pipeline is difficult to bypass it. △ Less

Submitted 27 December, 2022; originally announced December 2022.

Comments: Accepted by IEEE Conference on Secure and Trustworthy Machine Learning 2023

HZO-based FerroNEMS MAC for In-Memory Computing

Authors: Shubham Jadhav, Ved Gund, Benyamin Davaji, Debdeep Jena, Huili, Xing, Amit Lal

Abstract: This paper demonstrates a hafnium zirconium oxide (HZO)-based ferroelectric NEMS unimorph as the fundamental building block for very low-energy capacitive readout in-memory computing. The reported device consists of a 250 $μ$m $\times$ 30 $μ$m unimorph cantilever with 20 nm thick ferroelectric HZO on 1 $μ$m $SiO_2$.Partial ferroelectric switching in HZO achieves analog programmable control of the… ▽ More This paper demonstrates a hafnium zirconium oxide (HZO)-based ferroelectric NEMS unimorph as the fundamental building block for very low-energy capacitive readout in-memory computing. The reported device consists of a 250 $μ$m $\times$ 30 $μ$m unimorph cantilever with 20 nm thick ferroelectric HZO on 1 $μ$m $SiO_2$.Partial ferroelectric switching in HZO achieves analog programmable control of the piezoelectric coefficient ($d_{31}$) which serves as the computational weight for multiply-accumulate (MAC) operations. The displacement of the piezoelectric unimorph was recorded by actuating the device with different input voltages $V_{in}$. The resulting displacement was measured as a function of the ferroelectric programming/poling voltage $V_p$. The slopes of central beam displacement ($δ_{max}$) vs $V_{in}$ were measured to be between 182.9nm/V (for -8 $V_p$) and -90.5nm/V (for 8 $V_p$), demonstrating that $V_p$ can be used to change the direction of motion of the beam. The resultant ($δ_{max}$) from AC actuation is in the range of -18 to 36 nm and is a scaled product of the input voltage and programmed $d_{31}$ (governed by the $V_p$). The multiplication function serves as the fundamental unit for MAC operations with the ferroelectric NEMS unimorph. The displacement from many such beams can be added by summing the capacitance changes, providing a pathway to implement a multi-input and multi-weight neuron. A scaling and fabrication analysis suggests that this device can be CMOS compatible, achieving high in-memory computational throughput. △ Less

Submitted 12 August, 2022; originally announced August 2022.

MonkeyDB: Effectively Testing Correctness against Weak Isolation Levels

Authors: Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, Akash Lal

Abstract: Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale storage systems for storing and retrieving data. In the presence of concurrent accesses, these storage systems trade off isolation for performance. The weaker the isolation level, the more behaviors a storage system is allowed to exhibit and it is up to the developer to ensure that… ▽ More Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale storage systems for storing and retrieving data. In the presence of concurrent accesses, these storage systems trade off isolation for performance. The weaker the isolation level, the more behaviors a storage system is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors. However, these weak behaviors only occur rarely in practice, that too outside the control of the application, making it difficult for developers to test the robustness of their code against weak isolation levels. This paper presents MonkeyDB, a mock storage system for testing storage-backed applications. MonkeyDB supports a Key-Value interface as well as SQL queries under multiple isolation levels. It uses a logical specification of the isolation level to compute, on a read operation, the set of all possible return values. MonkeyDB then returns a value randomly from this set. We show that MonkeyDB provides good coverage of weak behaviors, which is complete in the limit. We test a variety of applications for assertions that fail only under weak isolation. MonkeyDB is able to break each of those assertions in a small number of attempts. △ Less

Submitted 3 March, 2021; originally announced March 2021.

Explainable Deep Behavioral Sequence Clustering for Transaction Fraud Detection

Authors: Wei Min, Weiming Liang, Hang Yin, Zhurong Wang, Mei Li, Alok Lal

Abstract: In e-commerce industry, user behavior sequence data has been widely used in many business units such as search and merchandising to improve their products. However, it is rarely used in financial services not only due to its 3V characteristics - i.e. Volume, Velocity and Variety - but also due to its unstructured nature. In this paper, we propose a Financial Service scenario Deep learning based Be… ▽ More In e-commerce industry, user behavior sequence data has been widely used in many business units such as search and merchandising to improve their products. However, it is rarely used in financial services not only due to its 3V characteristics - i.e. Volume, Velocity and Variety - but also due to its unstructured nature. In this paper, we propose a Financial Service scenario Deep learning based Behavior data representation method for Clustering (FinDeepBehaviorCluster) to detect fraudulent transactions. To utilize the behavior sequence data, we treat click stream data as event sequence, use time attention based Bi-LSTM to learn the sequence embedding in an unsupervised fashion, and combine them with intuitive features generated by risk experts to form a hybrid feature representation. We also propose a GPU powered HDBSCAN (pHDBSCAN) algorithm, which is an engineering optimization for the original HDBSCAN algorithm based on FAISS project, so that clustering can be carried out on hundreds of millions of transactions within a few minutes. The computation efficiency of the algorithm has increased 500 times compared with the original implementation, which makes flash fraud pattern detection feasible. Our experimental results show that the proposed FinDeepBehaviorCluster framework is able to catch missed fraudulent transactions with considerable business values. In addition, rule extraction method is applied to extract patterns from risky clusters using intuitive features, so that narrative descriptions can be attached to the risky clusters for case investigation, and unknown risk patterns can be mined for real-time fraud detection. In summary, FinDeepBehaviorCluster as a complementary risk management strategy to the existing real-time fraud detection engine, can further increase our fraud detection and proactive risk defense capabilities. △ Less

Submitted 11 January, 2021; originally announced January 2021.

Comments: Accepted by AAAI2021 KDF Workshop

A Novel Approach of using AR and Smart Surgical Glasses Supported Trauma Care

Authors: Anurag Lal, Ming-Hsien Hu, Pei-Yuan Lee, Min Liang Wang

Abstract: BACKGROUND: Augmented reality (AR) is gaining popularity in varying field such as computer gaming and medical education fields. However, still few of applications in real surgeries. Orthopedic surgical applications are currently limited and underdeveloped. - METHODS: The clinic validation was prepared with the currently available AR equipment and software. A total of 1 Vertebroplasty, 2 ORIF Pelvi… ▽ More BACKGROUND: Augmented reality (AR) is gaining popularity in varying field such as computer gaming and medical education fields. However, still few of applications in real surgeries. Orthopedic surgical applications are currently limited and underdeveloped. - METHODS: The clinic validation was prepared with the currently available AR equipment and software. A total of 1 Vertebroplasty, 2 ORIF Pelvis fracture, 1 ORIF with PFN for Proximal Femoral Fracture, 1 CRIF for distal radius fracture and 2 ORIF for Tibia Fracture cases were performed with fluoroscopy combined with AR smart surgical glasses system. - RESULTS: A total of 1 Vertebroplasty, 2 ORIF Pelvis fracture, 1 ORIF with PFN for Proximal Femoral Fracture, 1 CRIF for distal radius fracture and 2 ORIF for Tibia Fracture cases are performed to evaluate the benefits of AR surgery. Among the AR surgeries, surgeons wear the smart surgical are lot reduce of eyes of turns to focus on the monitors. This paper shows the potential ability of augmented reality technology for trauma surgery. △ Less

Submitted 25 May, 2020; originally announced May 2020.

Comments: 10 pages, 9 Figures, Conference. arXiv admin note: text overlap with arXiv:1801.01560 by other authors

Distributed Bounded Model Checking

Authors: Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, Akash Lal

Abstract: Program verification is a resource-hungry task. This paper looks at the problem of parallelizing SMT-based automated program verification, specifically bounded model-checking, so that it can be distributed and executed on a cluster of machines. We present an algorithm that dynamically unfolds the call graph of the program and frequently splits it to create sub-tasks that can be solved in parallel.… ▽ More Program verification is a resource-hungry task. This paper looks at the problem of parallelizing SMT-based automated program verification, specifically bounded model-checking, so that it can be distributed and executed on a cluster of machines. We present an algorithm that dynamically unfolds the call graph of the program and frequently splits it to create sub-tasks that can be solved in parallel. The algorithm is adaptive, controlling the splitting rate according to available resources, and also leverages information from the SMT solver to split where most complexity lies in the search. We implemented our algorithm by modifying CORRAL, the verifier used by Microsoft's Static Driver Verifier (SDV), and evaluate it on a series of hard SDV benchmarks. △ Less

Submitted 16 May, 2020; originally announced May 2020.

Building Reliable Cloud Services Using P# (Experience Report)

Authors: Pantazis Deligiannis, Narayanan Ganapathy, Akash Lal, Shaz Qadeer

Abstract: Cloud services must typically be distributed across a large number of machines in order to make use of multiple compute and storage resources. This opens the programmer to several sources of complexity such as concurrency, order of message delivery, lossy network, timeouts and failures, all of which impose a high cognitive burden. This paper presents evidence that technology inspired by formal-met… ▽ More Cloud services must typically be distributed across a large number of machines in order to make use of multiple compute and storage resources. This opens the programmer to several sources of complexity such as concurrency, order of message delivery, lossy network, timeouts and failures, all of which impose a high cognitive burden. This paper presents evidence that technology inspired by formal-methods, delivered as part of a programming framework, can help address these challenges. In particular, we describe the experience of several engineering teams in Microsoft Azure that used the open-source P# programming framework to build multiple reliable cloud services. P# imposes a principled design pattern that allows writing formal specifications alongside production code that can be systematically tested, without deviating from routine engineering practices. Engineering teams that have been using P# have reported dramatically increased productivity (in time taken to push new features to production) as well as services that have been running live for months without any issues in features developed and tested with P#. △ Less

Submitted 12 February, 2020; originally announced February 2020.

Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript)

Authors: Peizun Liu, Thomas Wahl, Akash LaL

Abstract: We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines queue-bounded exploration with a convergence test: if the sequence of certain abstractions of the reachable states, for increasing queue bound… ▽ More We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines queue-bounded exploration with a convergence test: if the sequence of certain abstractions of the reachable states, for increasing queue bounds k, converges, we can prove any property of the program that is preserved by the abstraction. If the abstract state space is finite, convergence is guaranteed; the challenge is to catch the point k_max where it happens. We further demonstrate how simple invariants formulated over the concrete domain can be used to eliminate spurious abstract states, which otherwise prevent the sequence from converging. We have implemented our technique for the P programming language for event-driven programs. We show experimentally that the sequence of abstractions often converges fully automatically, in hard cases with minimal designer support in the form of sequentially provable invariants, and that this happens for a value of k_max small enough to allow the method to succeed in practice. △ Less

Submitted 23 May, 2019; originally announced May 2019.

Comments: This is an extended technical report of a paper published in CAV 2019

Reliable State Machines: A Framework for Programming Reliable Cloud Services

Authors: Suvam Mukherjee, Nitin John Raj, Krishnan Govindraj, Pantazis Deligiannis, Chandramouleswaran Ravichandran, Akash Lal, Aseem Rastogi, Raja Krishnaswamy

Abstract: Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by construction. Using our framework, a programmer can build an application as several (possibly distributed) RSMs that communicate with each other via messages, muc… ▽ More Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by construction. Using our framework, a programmer can build an application as several (possibly distributed) RSMs that communicate with each other via messages, much in the style of actor-based programming. Each RSM is additionally fault-tolerant by design and offers the illusion of being "always-alive". An RSM is guaranteed to process each input request exactly once, as one would expect in a failure-free environment. The RSM runtime automatically takes care of persisting state and rehydrating it on a failover. We present the core syntax and semantics of RSMs, along with a formal proof of failure-transparency. We provide an implementation of the RSM framework and runtime on the .NET platform for deploying services to Microsoft Azure. We carried out an extensive performance evaluation on micro-benchmarks to show that one can build high-throughput applications with RSMs. We also present a case study where we rewrote a significant part of a production cloud service using RSMs. The resulting service has simpler code and exhibits production-grade performance. △ Less

Submitted 27 February, 2019; v1 submitted 25 February, 2019; originally announced February 2019.

Comments: R1: This replacement contains minor formatting improvements over the original R2: Anonymized "popular cloud service provider" phrase replaced with "Microsoft Azure"

Vector Quantized Spectral Clustering applied to Soybean Whole Genome Sequences

Authors: Aditya A. Shastri, Kapil Ahuja, Milind B. Ratnaparkhe, Aditya Shah, Aishwary Gagrani, Anant Lal

Abstract: We develop a Vector Quantized Spectral Clustering (VQSC) algorithm that is a combination of Spectral Clustering (SC) and Vector Quantization (VQ) sampling for grou** Soybean genomes. The inspiration here is to use SC for its accuracy and VQ to make the algorithm computationally cheap (the complexity of SC is cubic in-terms of the input size). Although the combination of SC and VQ is not new, the… ▽ More We develop a Vector Quantized Spectral Clustering (VQSC) algorithm that is a combination of Spectral Clustering (SC) and Vector Quantization (VQ) sampling for grou** Soybean genomes. The inspiration here is to use SC for its accuracy and VQ to make the algorithm computationally cheap (the complexity of SC is cubic in-terms of the input size). Although the combination of SC and VQ is not new, the novelty of our work is in develo** the crucial similarity matrix in SC as well as use of k-medoids in VQ, both adapted for the Soybean genome data. We compare our approach with commonly used techniques like UPGMA (Un-weighted Pair Graph Method with Arithmetic Mean) and NJ (Neighbour Joining). Experimental results show that our approach outperforms both these techniques significantly in terms of cluster quality (up to 25% better cluster quality) and time complexity (order of magnitude faster). △ Less

Submitted 30 September, 2018; originally announced October 2018.

Comments: 10 Pages, 3 Tables, 2 Figures

MSC Class: 68T01; 68T10; 68W40

CONFLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code

Authors: Ajay Brahmakshatriya, Piyus Kedia, Derrick Paul McKee, Pratik Bhatu, Deepak Garg, Akash Lal, Aseem Rastogi

Abstract: We present an instrumenting compiler for enforcing data confidentiality in low-level applications (e.g. those written in C) in the presence of an active adversary. In our approach, the programmer marks secret data by writing lightweight annotations on top-level definitions in the source code. The compiler then uses a static flow analysis coupled with efficient runtime instrumentation, a custom mem… ▽ More We present an instrumenting compiler for enforcing data confidentiality in low-level applications (e.g. those written in C) in the presence of an active adversary. In our approach, the programmer marks secret data by writing lightweight annotations on top-level definitions in the source code. The compiler then uses a static flow analysis coupled with efficient runtime instrumentation, a custom memory layout, and custom control-flow integrity checks to prevent data leaks even in the presence of low-level attacks. We have implemented our scheme as part of the LLVM compiler. We evaluate it on the SPEC micro-benchmarks for performance, and on larger, real-world applications (including OpenLDAP, which is around 300KLoC) for programmer overhead required to restructure the application when protecting the sensitive data such as passwords. We find that performance overheads introduced by our instrumentation are moderate (average 12% on SPEC), and the programmer effort to port OpenLDAP is only about 160 LoC. △ Less

Submitted 13 March, 2019; v1 submitted 30 November, 2017; originally announced November 2017.

Comments: Technical report for CONFLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code, appearing at EuroSys 2019

Precise Null Pointer Analysis Through Global Value Numbering

Authors: Ankush Das, Akash Lal

Abstract: Precise analysis of pointer information plays an important role in many static analysis techniques and tools today. The precision, however, must be balanced against the scalability of the analysis. This paper focusses on improving the precision of standard context and flow insensitive alias analysis algorithms at a low scalability cost. In particular, we present a semantics-preserving program tran… ▽ More Precise analysis of pointer information plays an important role in many static analysis techniques and tools today. The precision, however, must be balanced against the scalability of the analysis. This paper focusses on improving the precision of standard context and flow insensitive alias analysis algorithms at a low scalability cost. In particular, we present a semantics-preserving program transformation that drastically improves the precision of existing analyses when deciding if a pointer can alias NULL. Our program transformation is based on Global Value Numbering, a scheme inspired from compiler optimizations literature. It allows even a flow-insensitive analysis to make use of branch conditions such as checking if a pointer is NULL and gain precision. We perform experiments on real-world code to measure the overhead in performing the transformation and the improvement in the precision of the analysis. We show that the precision improves from 86.56% to 98.05%, while the overhead is insignificant. △ Less

Submitted 19 February, 2017; originally announced February 2017.

Comments: 17 pages, 1 section in Appendix

Structured illumination microscopy image reconstruction algorithm

Authors: Amit Lal, Chunyan Shan, Peng Xi

Abstract: Structured illumination microscopy (SIM) is a very important super-resolution microscopy technique, which provides high speed super-resolution with about two-fold spatial resolution enhancement. Several attempts aimed at improving the performance of SIM reconstruction algorithm have been reported. However, most of these highlight only one specific aspect of the SIM reconstruction -- such as the de… ▽ More Structured illumination microscopy (SIM) is a very important super-resolution microscopy technique, which provides high speed super-resolution with about two-fold spatial resolution enhancement. Several attempts aimed at improving the performance of SIM reconstruction algorithm have been reported. However, most of these highlight only one specific aspect of the SIM reconstruction -- such as the determination of the illumination pattern phase shift accurately -- whereas other key elements -- such as determination of modulation factor, estimation of object power spectrum, Wiener filtering frequency components with inclusion of object power spectrum information, translocating and the merging of the overlap** frequency components -- are usually glossed over superficially. In addition, most of the work reported lie scattered throughout the literature and a comprehensive review of the theoretical background is found lacking. The purpose of the present work is two-fold: 1) to collect the essential theoretical details of SIM algorithm at one place, thereby making them readily accessible to readers for the first time; and 2) to provide an open source SIM reconstruction code (named OpenSIM), which enables users to interactively vary the code parameters and study it's effect on reconstructed SIM image. △ Less

Submitted 18 February, 2016; originally announced February 2016.

Comments: OpenSIM code may be downloaded from: https://github.com/LanMai/OpenSIM

Automatically finding atomic regions for fixing bugs in Concurrent programs

Authors: Saurabh Joshi, Akash Lal

Abstract: This paper presents a technique for automatically constructing a fix for buggy concurrent programs: given a concurrent program that does not satisfy user-provided assertions, we infer atomic blocks that fix the program. An atomic block protects a piece of code and ensures that it runs without interruption from other threads. Our technique uses a verification tool as a subroutine to find the smalle… ▽ More This paper presents a technique for automatically constructing a fix for buggy concurrent programs: given a concurrent program that does not satisfy user-provided assertions, we infer atomic blocks that fix the program. An atomic block protects a piece of code and ensures that it runs without interruption from other threads. Our technique uses a verification tool as a subroutine to find the smallest atomic regions that remove all bugs in a given program. Kee** the atomic regions small allows for maximum concurrency. We have implemented our approach in a tool called AtomicInf. A user of AtomicInf can choose between strong and weak atomicity semantics for the inferred fix. While the former is simpler to find, the latter provides more information about the bugs that got fixed. We ran AtomicInf on several benchmarks and came up with the smallest and the most precise atomic regions in all of them. We implemented an earlier technique to our setting and observed that AtomicInf is 1.7 times faster on an average as compared to an earlier approach. △ Less

Submitted 7 March, 2014; originally announced March 2014.

Comments: 16 pages, 6 figures, 1 table

Variable and Thread Bounding for Systematic Testing of Multithreaded Programs

Authors: Sandeep Bindal, Sorav Bansal, Akash Lal

Abstract: Previous approaches to systematic state-space exploration for testing multi-threaded programs have proposed context-bounding and depth-bounding to be effective ranking algorithms for testing multithreaded programs. This paper proposes two new metrics to rank thread schedules for systematic state-space exploration. Our metrics are based on characterization of a concurrency bug using v (the minimum… ▽ More Previous approaches to systematic state-space exploration for testing multi-threaded programs have proposed context-bounding and depth-bounding to be effective ranking algorithms for testing multithreaded programs. This paper proposes two new metrics to rank thread schedules for systematic state-space exploration. Our metrics are based on characterization of a concurrency bug using v (the minimum number of distinct variables that need to be involved for the bug to manifest) and t (the minimum number of distinct threads among which scheduling constraints are required to manifest the bug). Our algorithm is based on the hypothesis that in practice, most concurrency bugs have low v (typically 1- 2) and low t (typically 2-4) characteristics. We iteratively explore the search space of schedules in increasing orders of v and t. We show qualitatively and empirically that our algorithm finds common bugs in fewer number of execution runs, compared with previous approaches. We also show that using v and t improves the lower bounds on the probability of finding bugs through randomized algorithms. Systematic exploration of schedules requires instrumenting each variable access made by a program, which can be very expensive and severely limits the applicability of this approach. Previous work [5, 19] has avoided this problem by interposing only on synchronization operations (and ignoring other variable accesses). We demonstrate that by using variable bounding (v) and a static imprecise alias analysis, we can interpose on all variable accesses (and not just synchronization operations) at 10-100x less overhead than previous approaches. △ Less

Submitted 5 February, 2013; v1 submitted 11 July, 2012; originally announced July 2012.

Group Signature Schemes Using Braid Groups

Authors: Tony Thomas, Arbind Kumar Lal

Abstract: Artin's braid groups have been recently suggested as a new source for public-key cryptography. In this paper we propose the first group signature schemes based on the conjugacy problem, decomposition problem and root problem in the braid groups which are believed to be hard problems. Artin's braid groups have been recently suggested as a new source for public-key cryptography. In this paper we propose the first group signature schemes based on the conjugacy problem, decomposition problem and root problem in the braid groups which are believed to be hard problems. △ Less

Submitted 17 February, 2006; originally announced February 2006.

Undeniable Signature Schemes Using Braid Groups

Authors: Tony Thomas, Arbind Kumar Lal

Abstract: Artin's braid groups have been recently suggested as a new source for public-key cryptography. In this paper we propose the first undeniable signature schemes using the conjugacy problem and the decomposition problem in the braid groups which are believed to be hard problems. Artin's braid groups have been recently suggested as a new source for public-key cryptography. In this paper we propose the first undeniable signature schemes using the conjugacy problem and the decomposition problem in the braid groups which are believed to be hard problems. △ Less

Submitted 13 January, 2006; originally announced January 2006.

On Expanders Graphs: Parameters and Applications

Authors: H. L. Janwa A. K. Lal

Abstract: We give a new lower bound on the expansion coefficient of an edge-vertex graph of a $d$-regular graph. As a consequence, we obtain an improvement on the lower bound on relative minimum distance of the expander codes constructed by Sipser and Spielman. We also derive some improved results on the vertex expansion of graphs that help us in improving the parameters of the expander codes of Alon, Bru… ▽ More We give a new lower bound on the expansion coefficient of an edge-vertex graph of a $d$-regular graph. As a consequence, we obtain an improvement on the lower bound on relative minimum distance of the expander codes constructed by Sipser and Spielman. We also derive some improved results on the vertex expansion of graphs that help us in improving the parameters of the expander codes of Alon, Bruck, Naor, Naor, and Roth. △ Less

Submitted 25 June, 2004; originally announced June 2004.

Comments: Submitted to SIAM J. DAM on Feb. 1, 2001