Diego Garbervetsky

Man Zhang, Tao Yue, Nazareno M. Aguirre et al.

Complex software systems such as autonomous vehicles, robotics increasingly interact with dynamic physical, cyber, and social environments. Reasoning about their behavior, maintaining them under continuous change, and evolving them safely require trustworthy knowledge about the system, its assumptions, and its operating context. Knowledge models (KMs) provide a practical basis for such reasoning, but they may themselves become incomplete, inconsistent, or outdated as systems evolve. This paper presents TrustModel, a vision for the agentic generation and evolution of living KMs. TrustModel comprises three agentic subsystems: Modeling, for constructing and updating KMs; Conformance, for assessing their alignment with the system and its environment; and Evolution, for generating guidance to keep KMs synchronized with emerging changes. We demonstrate how TrustModel can be instantiated for model-based testing and discuss its potential for supporting other MDE activities, such as requirements and assumption monitoring, architectural drift tracking, and change impact assessment. Overall, TrustModel positions living KMs as a foundation for dependable engineering of continuously evolving software systems.

Agustín Balestra, Agustín Nolasco, Facundo Molina et al.

Contract assertions, such as preconditions, postconditions, and invariants, play a crucial role in software development, enabling applications such as program verification, test generation, and debugging. Despite their benefits, the adoption of contract assertions is limited, due to the difficulty of manually producing such assertions. Dynamic analysis-based approaches, such as Daikon, can aid in this task by inferring expressive assertions from execution traces. However, a fundamental weakness of these methods is their reliance on the thoroughness of the test suites used for dynamic analysis. When these test suites do not contain sufficiently diverse tests, the inferred assertions are often not generalizable, leading to a high rate of invalid candidates (false positives) that must be manually filtered out. In this paper, we explore the use of large language models (LLMs) to automatically generate tests that attempt to invalidate generated assertions. Our results show that state-of-the-art LLMs can generate effective counterexamples that help to discard up to 11.68\% of invalid assertions inferred by SpecFuzzer. Moreover, when incorporating these LLM-generated counterexamples into the dynamic analysis process, we observe an improvement of up to 7\% in precision of the inferred specifications, with respect to the ground-truths gathered from the evaluation benchmarks, without affecting recall.

Saikat Dutta, Diego Garbervetsky, Shuvendu Lahiri et al.

Static analysis has established itself as a weapon of choice for detecting security vulnerabilities. Taint analysis in particular is a very general and powerful technique, where security policies are expressed in terms of forbidden flows, either from untrusted input sources to sensitive sinks (in integrity policies) or from sensitive sources to untrusted sinks (in confidentiality policies). The appeal of this approach is that the taint-tracking mechanism has to be implemented only once, and can then be parameterized with different taint specifications (that is, sets of sources and sinks, as well as any sanitizers that render otherwise problematic flows innocuous) to detect many different kinds of vulnerabilities. But while techniques for implementing scalable inter-procedural static taint tracking are fairly well established, crafting taint specifications is still more of an art than a science, and in practice tends to involve a lot of manual effort. Past work has focussed on automated techniques for inferring taint specifications for libraries either from their implementation or from the way they tend to be used in client code. Among the latter, machine learning-based approaches have shown great promise. In this work we present our experience combining an existing machine-learning approach to mining sink specifications for JavaScript libraries with manual taint modelling in the context of GitHub's CodeQL analysis framework. We show that the machine-learning component can successfully infer many new taint sinks that either are not part of the manual modelling or are not detected due to analysis incompleteness. Moreover, we present techniques for organizing sink predictions using automated ranking and code-similarity metrics that allow an analysis engineer to efficiently sift through large numbers of predictions to identify true positives.

Rodrigo Castaño, Victor Braberman, Diego Garbervetsky et al.

Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly effective, leading to a number of high-profile success stories. However, widespread adoption remains unlikely in the short term and one of the remaining obstacles in that direction is the vast number of instances which software model checkers cannot fully analyze within reasonable memory and CPU bounds. The majority of verification tools fail to provide a measure of progress or any intermediate verification result when such situations occur. Inspired in the success that coverage metrics have achieved in industry, we propose to adapt the definition of coverage to the context of verification. We discuss some of the challenges in pinning down a definition that resembles the deeply rooted semantics of test coverage. Subsequently we propose a definition for a broad family of verification techniques: those based on Abstract Reachability Trees. Moreover, we discuss a general approach to computing an under-approximation of such metric and a specific heuristic to improve the performance. Finally, we conduct an empirical evaluation to assess the viability of our approach.

Rodrigo Castaño, Victor Braberman, Diego Garbervetsky et al.

Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checkers fail often and usually do not provide any information on what was effectively checked. The purpose of this work is to provide a conceptual framing to extend software model checkers in a way that allows users to access information about incomplete checks. We characterize the information that model checkers themselves can provide, in terms of analyzed traces, i.e. sequences of statements, and safe cones, and present the notion of execution reports, which we also formalize. We instantiate these concepts for a family of techniques based on Abstract Reachability Trees and implement the approach using the software model checker CPAchecker. We evaluate our approach empirically and provide examples to illustrate the execution reports produced and the information that can be extracted.

Pablo Bendersky, Juan Pablo Galeotti, Diego Garbervetsky

We present an extension to the DynAlloy tool to navigate DynAlloy counterexamples: the DynAlloy Visualizer. The user interface mimics the functionality of a programming language debugger. Without this tool, a DynAlloy user is forced to deal with the internals of the Alloy intermediate representation in order to debug a flaw in her model.

Rodrigo Castaño, Juan Pablo Galeotti, Diego Garbervetsky et al.

In this paper we present an approach to check resource consumption contracts using an off-the-shelf static analyzer. We propose a set of annotations to support resource usage specifications, in particular, dynamic memory consumption constraints. Since dynamic memory may be recycled by a memory manager, the consumption of this resource is not monotone. The specification language can express both memory consumption and lifetime properties in a modular fashion. We develop a proof-of-concept implementation by extending Code Contracts' specification language. To verify the correctness of these annotations we rely on the Code Contracts static verifier and a points-to analysis. We also briefly discuss possible extensions of our approach to deal with non-linear expressions.