The paper describes static analysis of map in the Go language for dereferencing a null pointer when extracting a key from a map. The work has been done within the Svace static analyzer. We begin with introducing Svace intermediate representation and algorithms. Then we describe the IR changes needed for modeling Go maps and their semantics. We explain how intraprocedural analysis is performed and how the null dereference detector works. Then we proceed with a summary-based interprocedural analysis. We show evaluation results on a wide range of open source projects.

Many modern static analysis tools provide toolkits that allow creation of custom checkers by end users. The majority of existing solutions choose AST-based approaches to provide a simpler declarative API. Solutions based on dataflow analysis or symbolic execution use complex explicit APIs that require much more expertise to achieve decent results compared to AST-based checkers. Even though the latter approach is much more powerful simplicity of the former made it much more prevalent.In this paper we introduce SvaceAPI a tool to write checkers based on symbolic execution in a declarative way. We describe a simple pattern-based API that leverages symbolic execution and attributes provided by Svace. Testing the API on a couple of checkers and open source programs across the variety of languages showed the same quality results as for built-in Svace checkers without noticeable performance regressions.

In the last 15 years many dedicated leak detection tools utilizing novel approaches were designed. Unfortunately, most of them are hard to implement and fully utilize in the scope of a multi-purpose industrial analyzer. In this paper we present a full-fledged approach to static analysis through the lens of resource leak detection. We show how general analysis architecture without much of a focus for specific defects can still be effective at finding leaks both in terms of performance and number of warnings. We briefly describe an overall structure of the Svace static analyzer and how it achieves context and path sensitivities as well as interprocedurality, while allowing for checking many program properties and being highly extensible. We also show how to use this system to implement leak detection algorithm with including a few unique extensions that we have never seen in other instruments. Our test results show a low false positive rate, relatively good performance for a multi-detector static analyzer and great scalability potential both in terms of adding new algorithms and analyzing millions of lines of code.

The paper describes a static analyzer for finding defects in Scala programs. The proposed analysis scheme uses JVM bytecode produced during compilation. The generated bytecode is used as an input for inter-procedural static analyzer Svace. In contrast to the analysis of other languages supported by Svace, in this work we describe an approach that does not require compiler modifications and therefore simplifies language support. This approach can also be used in static analyzers that aim to support a large number of programming languages.

This paper describes a static analysis tool for finding defects, analyzing metrics and relations for programs written in the Kotlin language. The approach is implemented in the Svace static analyzer developed at the Ivannikov Institute for System Programming of the Russian Academy of Sciences. The paper focuses on the problems we faced during the implementation, the approaches we used to solve them, and the experimental results for the tool we built. The tool not only supports Kotlin but is also capable of analyzing mixed projects that use both Java and Kotlin. We hope that this paper will be useful to static analysis developers and language designers.

This paper presents a method for build interception of Go projects and utilizing the intercepted information for building an intermediate representation used in a static analyzer. The paper discusses two approaches: handling invocations of the higher-level go build command and handling invocations of the lower-level compile tool. The second solution is applicable not only to the built-in Go build system but also to other build systems that directly utilize the low-level compile tool, such as Bazel, Please, Pants. It also covers compilations involving CGO.

The paper describes a unified representation for an abstract syntax tree (AST) suitable for static analysis of several programming languages. The proposed analysis scheme consists of saving an intermediate representation in the form of a unified AST from compilers of the corresponding languages and subsequent analysis of the saved trees. We have implemented this described representation for Java, Kotlin and Python. The unified AST analyzer has 27 checkers. In the paper we present structure and entities of our unified AST, provide more details regarding language specifics that have to be reflected in the UAST representation. We give extensive experimental results that show UAST generation and analysis speed, analysis quality, and comparison with the old scheme of analyzing compiler ASTs where applicable. As a result, we see that we observe some degradation of analysis speed, but we pay it for the separation of AST construction and checkers’ implementation. This separation allows easier support of many languages in the analyzer, where one can just generate UAST and support the required checker once within the UAST infrastructure instead of implementing a checker once per language.

This paper describes static analysis for the languages with exception handling. A low level intermediate representation, which supports exceptions, is proposed in this study. Data flow analyses for unreachable code detection were described. А general scheme of static analysis that takes exception related paths into account was given. The algorithms were implemented as a part of the static analysis tool Svace for C++, Java and Kotlin languages.

We present an interprocedural static analysis to detect errors in the Go source code. The analysis supports most of the language features, while the main focus of the paper is closures and defer statements. The analysis we have developed demonstrates good scalability and performance. It is able to analyze a project of 1.1 million lines in 12 minutes.

We propose a points-to analysis that can recover targets for function pointer calls, virtual calls and method calls for using in a static analysis. We use a flow-insensitive analysis, and the analysis results are intended for flow- and path-sensitive analysis which can improve the initial analysis precision within a single function. We implemented the proposed approach in a static analyzer for finding errors in C, C++, Go, Java and Kotlin programs. The devirtualization algorithm is fast enough and spends less than 6% of the total analysis time. It can work for projects like Tizen 7 with 27.5 MLoc of source code.

This paper describes a static analysis tool for soft-ware defects detection in source code written in Go language. We developed a fast lightweight AST-based analyzer (GOA) to support detection of syntactic-level issues (linter) and a powerful interprocedural summary-based analyzer (SVENG) with its own intermediate representation.

In this paper, we overview the approaches and techniques employed by the Svace static analysis tool for intraprocedural analysis. This analysis implies the traversal of the control flow graph, symbolic execution with state merging, analysis of a number of paths in functions with loops, simultaneous run of all analyzers, modeling of accessible memory cells, and value numbering.

In recent years, the popularity of the Go programming language has been growing. However, currently, there are only lightweight static analyzers (linters) available for Go. We fill this gap by adapting the Svace static analyzer for Go programs. We implement an interprocedural and intermodular static analyzer that possesses both flow sensitivity and path sensitivity. To evaluate its performance, we use ten open source projects. The sixteen evaluated checkers emitted 6817 warnings with 76% true positive rate.

This paper is dedicated to finding taint-based errors in the source code of programs, i.e., errors caused by unsafe use of data from external sources, which could potentially be modified by a malefactor. The interprocedural static analyzer Svace is used as a basis. The analyzer searches for both program defects and suspicious points where the logic of the program may be corrupted. The goal is to find as many errors as possible at an acceptable speed and low false positive rate (<20–35%). For this purpose, Svace builds, with the help of a modified compiler, a low-level typed intermediate representation, which is input to the main SvEng analyzer. The analyzer constructs a call graph and then carries out summary-based analysis. In this analysis, functions are traversed according to the call graph, starting from the leaves. Once a function is analyzed, its summary is created, which is then used to analyze call instructions. The analysis has both high speed and good scalability. Intraprocedural analysis is based on symbolic execution with state merging at join points. An SMT solver can be used to filter out infeasible paths for some checkers. In this case, the SMT solver is called only if an error is suspected. The analyzer has been extended to find defects of tainted data use. The checkers are implemented as plugins based on the source–sink scheme. The sources are calls of library functions that receive data from the outside of the program, as well as arguments of the main function. The sinks are accesses to arrays, uses of variables as steps or loop boundaries, and calls of functions that require checked arguments. Checkers that cover most of possible vulnerabilities for tainted integers and strings are implemented. To assess the coverage, the Juliet project is used. The false negative rate ranges from 46.31% to 81.17% with a small number of false positives.

The paper is dedicated to search for taint-based errors in the source code of programs, i.e. errors caused by unsafe use of data obtained from external sources, which could potentially be modified by an attacker. The interprocedural static analyzer Svace was used as a basis. The analyzer searches both for defects in the program and searches for suspicious places where the logic of the program may be violated. The goal is to find as many errors as possible at an acceptable speed and a low level of false positives (< 20-35%). To find errors, Svace with help of modified compiler builds a low-level typed intermediate representation, which is used as an input to the main SvEng analyzer. The analyzer builds a call graph and then performs summary-based analysis. In this analysis, the functions are traversed according to the call graph starting from the leaves. After analyzing the function, its summary is created, which will then be used to analyze the call instructions. The analysis has both high speed and good scalability. Intra-procedural analysis is based on symbolic execution with the union of states at merge points of paths. An SMT solver can be used to filter out infeasible paths for some checkers. In this case, the SMT-solver is called only if there is a suspicion of an error. The analyzer has been expanded to find defects of tainted data using. The checkers are implemented as plugins by using the source-sink scheme. The sources are calls of library functions that receive data from outside the program, as well as the arguments of the main function. Sinks are accessing to arrays, using variables as a step or loop boundary, calling functions that require checked arguments. Checkers covering most of the possible types of vulnerabilities for tainted integers and strings have been implemented. The Juliet project was used to assess the coverage. The false negative rate ranged from 46,31% to 81.17% with a small number of false positives.

The paper describes a static analysis for finding defects and computing metrics for programs written in the Kotlin language. The analysis is implemented in the Svace static analyzer developed at ISP RAS. The paper focuses on the problems we met during implementation, the approaches we used to solve them, and the experimental results for the tool we have built. The analyzer supports not only Kotlin analysis, but is also capable of analyzing mixed projects that use both Java and Kotlin languages. We hope that the paper might be useful to static analysis developers and language designers.

Проанализированы проблемы создания приемников градиента давления различных типов для использования в низкочастотном диапазоне, определяемые необходимостью достижения достаточной чувствительности к звуковому давлению в плоской волне, коэффициента деления дипольной характеристики направленности не хуже 26 дБ, динамического диапазона не менее 80–100 дБ. Теоретически оценены пределы применимости ПГД 2-гидрофонного (разностного) типов по волновым размерам. Разработаны высоко- эффективные ПГД инерционного и силового типов. Предложено комбинирование ПГД инерционного/силового и 2-гидрофонного типов в линейной антенне. The problems of development of pressure gradient sensors of various types for usage in low-frequency range are analyzed, which are connected to a necessity to provide acceptable sensitivity to sound pressure in a flat wave, minima of the dipole directivity pattern being nor less 26 dB, dynamic range being nor less 80–100 dB. The wavelength limits of acceptability of 2-hydrophone (differential) pressure gradient sensors are theoretically predicted. High effective pressure gradient sensors of inertial and force types are designed. It is suggested to combine a pressure gradient sensor of inertial or force type with the pressure gradient sensor of 2-hydrophone type in linear array.

Svace is a static analysis tool for bug detection in C/C++/Java source code. To analyze a program, Svace performs an intra-procedure analysis of individual functions, starting from the leaves of a call-graph and moving towards the roots, and uses summaries of previously analyzed procedures at call-cites. In this paper, we overview the approaches and techniques employed by Svace for the intra-procedural analysis. This phase is performed by an analyzer engine and an extensible set of detectors. The core engine employs a symbolic execution approach with state merging. It uses value numbering to reduce the set of symbolic expressions, maintains points-to relationship graph for memory modeling, and performs strong and weak updates of program values. Detectors are responsible for discovering and reporting bugs. They calculate different properties of program values using a variety of abstract domains. All detectors work simultaneously orchestrated by the engine. Svace analysis is unsound and employs a variety of heuristics to speed-up. We designed Svace to analyze big projects (several MLOCs) in just a few hours and report as many warnings as possible, while keeping a good quality of reports ≥ 65 of true positives). For example, Tizen 5.5 (20MLOC) analysis takes 8.6 hours and produces 18,920 warnings, more than 70% of which are true-positive.

The paper describes an extension to summary based static program analysis to find deadlock errors. Summary based analysis is a popular approach aimed at the detection of bugs in programs due to its high performance and scalability. At the same time, the implementation of deadlock detectors in such an analysis is nontrivial, because there is no information about the locks held higher in the call stack during the process of function intraprocedural analysis. A lock graph, which is built during the main analysis, is used to model the semantics of multithreaded programs. Lock graph is a modification of call graph which contains additional information about held locks. After the lock graph is built, the deadlock detector is launched. Both the construction of the lock graph and the deadlock detection algorithm do not require significant processor time. On the performed measurements, the total analysis time increased by 4%. Based on the results of the analysis of 8 open source projects in C/C++/Java with a total size of more than 14 million lines of code, the proposed algorithm showed a high level of true positives. The described algorithms were implemented in the Svace tool.