Abstract In VeriFuzz 1.4, we implemented two new techniques for checking Non-termination and Termination. VeriFuzz 1.4 won the Termination category of SV-COMP 2023.

For cloud native microservice monitoring and incident detection, companies and developers tend to largely focus only on generating logs, metrics, and traces at the application layer. However, in order to enable precise fault localization, it is necessary to access and correlate logs pertaining to a single end-user request across non-application layers as well, such as the load balancer at the front and the database at the back end. In this paper, we propose an observability library and an observability platform that addresses this problem and generates alerts that precisely point to fault locations. Logs at multiple layers are tagged with a common request identifier that helps in performing correlation. The observability platform is architected such that it lends itself to extensions to catch multiple types of errors and issues. The proposed observability platform has been tested on five open source benchmarks. The results confirm that our tool can be used deterministically and precisely to detect elusive issues.

Coverage Guided Fuzzing (CGF) is a greybox test generation technique. Bounded Model Checking (BMC) is a whitebox test generation technique. Both these have been highly successful at program coverage as well as error detection. It is well known that CGF fails to cover complex conditionals and deeply nested program points. BMC, on the other hand, fails to scale for programming features such as large loops and arrays. To alleviate the above problems, we propose (1) to combine BMC and CGF by using BMC for a short and potentially incomplete unwinding of a given program to generate effective initial test prefixes, which are then extended into complete test inputs for CGF to fuzz, and (2) in case BMC gets stuck even for the short unwinding, we automatically identify the reason, and rerun BMC with a corresponding remedial strategy. We call this approach as BMCFuzz and implemented it in the VeriFuzz framework. This implementation was experimentally evaluated by participating in Test-Comp 2021 and the results show that BMCFuzz is both effective and efficient at covering branches as well as exposing errors. In this paper, we present the details of BMCFuzz and our analysis of the experimental results.

Abstract We present VeriFuzz 1.2 with two new enhancements: (1) unroll the given program to a short depth and use BMC to produceincompletetest inputs, which are extended intocompleteinputs, and (2) if BMC fails for this short unrolling, automatically identify the reason and rerun BMC with a corresponding remedial strategy.

Unintended non-termination of programs could lead to attacks such as Denial-of-Service(DoS). Current testing techniques are not geared to detect such errors. Towards this, we present FuzzNT, a hybrid testing technique to check non-termination of C programs by combining Coverage Guided Fuzzing (CGF) and abstract interpretation based static analysis. Given a program P and the coverage test inputs generated using CGF, P is transformed into a set of specialized programs, each of which under-approximates P. Abstract interpretation is then used to check each of these smaller programs for non-termination. The key advantage of this approach for checking non-termination is that it reuses the test case corpus created during software development and maintenance. Our preliminary experimental evaluation of FuzzNT shows highly promising results.

Programs written in a high-level language such as C and Java, interleaved with declarative database processing and inter-service communication statements are common in Enterprise Information Systems (EIS). IT companies that offer re-engineering services for such EIS rely on manual analysis or code analysis tools to understand the flow of control and data within and across the programs during the reverse-engineering phase. Generally, the code analyzers are developed for commonly used programming languages, and lack support for analyzing database processing and inter-service communication statements. Therefore, such analysis tools cannot be readily re-used for re-engineering projects. In this paper, we share the key challenges of handling program analysis requirements for large embedded Structured Query Language (SQL) applications written in C language. We describe our approach to transform a program written in C and embedded SQL into a plain C program which can be automatically analyzed using any available C code analyzer that has no explicit support for domain specific extensions like SQL. We deployed the data dependency analysis based on our transformation approach as a feature in an industrial code analysis tool. We present the evaluation and results that show a precision improvement for slices as compared to the naïve translation provided by the standard pre-compiler.

Data migration from source to target information system is a critical step for modernizing information systems. Central to data migration is data transform that transforms the source system data into target system. In this paper we present a tool that assists the experts in creating the data transformation specification by (a) suggesting candidate field matches between the source and target data models using machine learning and knowledge representation, and (b) rules for the data transformation using program synthesis. It takes the expert’s feedback for the identified matches and synthesized rules and proposes new matches and transformation rules. We have executed our tool on real-life industrial data. Our schema matching recall at 5 is 0.76, while for the rule generator recall at 2 is 0.81.

VeriFuzz is a program aware fuzz testing tool, which combines the power of feedback-driven evolutionary fuzz testing with static analysis. VeriFuzz deploys lightweight static analysis to extract meaningful information about program behavior that can aid fuzzing based test-input generation to achieve coverage goals quickly. We use constraint-solver to generate an initial population of test-inputs. VeriFuzz could generate the maximum number of counterexamples for reachsafety category benchmarks in SV-COMP 2019 and in Test-Comp 2019 [ 16 ]. (All the terms in typewriter font are competition specific. See [ 15 ].)

Programs that process data that reside in files are widely used in varied domains, such as banking, healthcare, and web-traffic analysis. Precise static analysis of these programs in the context of software transformation and verification tasks is a challenging problem. Our key insight is that static analysis of file-processing programs can be made more useful if knowledge of the input file formats of these programs is made available to the analysis. We instantiate this idea to solve two practical problems - specializing the code of a program to a given “restricted” input file format, and verifying if a program “conforms” to a given input file format. We then discuss an implementation of our approach, and also empirical results on a set of real and realistic programs. The results are very encouraging in the terms of both scalability as well as precision of the approach.

Context sensitive inter-procedural dataflow analysis is a precise approach for static analysis of programs. It is very expensive in its full form. We propose a prefix approximation for context sensitive analysis, wherein a prefix of the full context stack is used to tag dataflow facts. Our technique, which is in contrast with suffix approximation that has been widely used in the literature, is designed to be more scalable when applied to programs with modular structure. We describe an instantiation of our technique in the setting of the classical call-strings approach for inter-procedural analysis. We analyzed several large enterprise programs using an implementation of our technique, and compared it with the fully context sensitive, context insensitive, as well as suffix-approximated variants of the call-strings approach. The precision of our technique was in general less than that of suffix approximation when measured on entire programs. However, the precision that it offered for outer-level procedures, which typically contain key business logic, was better, and its performance was much better.