arXiv subjects

Narges Shadab

Publications and source records attributed to Narges Shadab.

3 recordsLinked to original sources

arXiv2023

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

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.

cs.PL↗

arXiv2023

Inference of Resource Management Specifications

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.

cs.SE↗

arXiv2020

Temporal Logic of Composable Distributed Components

Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To modularly manage this complexity, network middleware has been traditionally built in layered stacks of components. We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to the operational semantics for stacks of distributed components. We successfully apply TLC to compose and verify a stack of fundamental distributed components.

cs.PL↗