Svace Specification Manual for Svace 4.0.250829

This document describes the way for customizing library or library or user functions behavior for the Svace static analyzer. Svace supports two main way to do this:

Specifications in Svace are manually created models for customizing functions behavior. Svace uses the data derived from specifications to make the analysis more precise. The following chapters introduce Svace analysis workflow, explain the way Svace uses specifications, and describe how they should be written.

Attributes are a mechanism in a programming language for providing additional information about a program to a compiler or static analyzer. Attributes are language dependent. Currently, Svace supports attributes for C/C++ and JVM languages (Java, Kotlin, Scala).

Svace Description

Svace is a static analysis tool for finding errors in programs written in C/C++, Java, and C#. The C# analyzer uses a separate engine that is technically on par with the main engine serving the first three languages. Support for Kotlin and Go languages is underway. Svace is developed in the Ivannikov Institute for System Programming of the Russian Academy of Sciences (ISP RAS).

Svace engine detects a wide variety of defects including null pointer dereference, memory and resource leaks, buffer overflow, unreachable code, tainted vulnerabilities, leaks of sensitive data, integer overflows, using unitialized data, concurrency errors, division by zero, use of freed memory and others. The engine workflow is as follows:

Svace engine uses the summary-based approach for performing interprocedural analysis. Such analysis traverses the call graph bottom up starting from leaves, meaning that when recursive cycles are broken, callees are analyzed before callers. When the intraprocedural function analysis pass completes, Svace builds the function summary which contains all information needed for analyzing this function’s callers.

Quite often the analyzer finds calls to unknown functions. Also some data may be omitted from a summary because of analysis imprecision or scalability tradeoffs. In such cases Svace can use external models for unknown or not fully precisely analyzed function. These models are written by an analyzer developer or a user and are called specifications. For example, a specification of the strlen function can include a note about unconditionally dereferencing its argument. Thus, an error will be reported by Svace when a null pointer is passed to that function, even if its source code is not available.

Svace function specification¹ is just an additional function definition written in the target language source code (C, C++, Java, Kotlin, Go). It describes the needed data about the function behavior in a compact and simple form. Along with the programming language constructs it can use calls to the predefined Svace special functions². Svace analysis engine processes the specifications similarly to other analyzed functions but uses the summary collected from the specifications prior to the functions original definitions.

Svace engine uses function specifications internally for modeling properties of standard libraries. This manual provides many examples from Svace specifications. Most of those examples are simplified versions of real specifications. All details that are irrelevant to the described mechanism are removed for simplicity.

Note: do not add specifications from this manual to Svace as the analyzer already contains their proper extended versions.

Specifications Overview

A specification is written as a function in the same language and with the same declaration as the modeled function. Svace analyzes the specification source code and uses it when analyzing calls to that function. Specifications allow describing properties of a function, its parameters or the return value. Svace engine will use those properties for modeling program semantics.

void *malloc(size_t size) {
    sf_set_trusted_sink_int(size); //size is tainted sink

    void *ptr;
    sf_overwrite(&ptr);  //'ptr' is initialized
    sf_set_alloc_possible_null(ptr, size); //'ptr' may be null
    sf_raw_new(ptr); //pointed memory by 'ptr' is not initialized
    sf_new(ptr, MALLOC_CATEGORY);
    //size of allocated buffer is 'size'
    sf_set_buf_size(ptr, size); 
    return ptr;
}

Important: User specifications take precedence over Svace internal specifications. It is unadvisable to create those for the functions already modeled by Svace as all effects of the Svace internal specification will be lost.

For analyzing specifications Svace first compiles them and then analyzes their source code representation in the same way as the regular functions. This means that specifications need to be correct programs so that they can be compiled without errors.

Svace uses a specification only for modeling a function call. If the project being analyzed contains the modeled function source code (e.g. a library that has own malloc implementation), Svace will analyze this function and report possible errors, but only its specification will be further used for analyzing calls to that function.

Important: Svace specifications affect all detectors and the engine algorithms. It is not possible to create specifications for a single checker.

Tutorial for C/C++

This chapter contains an example of using Svace function specifications for a simple program. The program uses a custom library for working with files and sending data via network.

An Example Program

//file program.c
//a user function that reads data from a file
int get_from_file(int handle);

//a user function that creates a buffer and returns its handle.
//the size parameter shouldn't be tainted
int create_my_buffer(int size);

void send_buffer(int bufHandle);

int handle = 0x700;

int read_data_from_file() {
    int data = get_from_file(handle);
    return data;
}

int main() {
    int val = read_data_from_file();
    //vulnerability: passing tainted data to a secure operation
    int bufHandle = create_my_buffer(val);

    send_buffer(bufHandle);
    return 0;
}

$ cat build_all.sh
#!/bin/bash
gcc -c program.c

$ svace init
$ svace build ./build_all.sh
$ svace analyze

Svace won’t find any vulnerabilities. The reason is that Svace doesn’t have any information about functions create_my_buffer and get_from_file.

Using Specifications

To provide information about user libraries we have to add Svace specifications. The lib.c file with specifications is like following:

int get_from_file(int handle) {
    int res;
    sf_overwrite(&res);//note: the & operator is used
    sf_set_tainted_int(res);
    return res;
}

int create_my_buffer(int size) {
    sf_set_trusted_sink_int(size);

    int res;
    sf_overwrite(&res);
    return res;
}

Note: Svace matches a specification and a modeled function via function name and argument number.

$ svace spec add lib.c

$ svace analyze

TAINTED_INT Integer value 'val' obtained from untrusted source at program.c:13 by calling function 'get_from_file' at program.c:8 without checking its bounds is used in a trusted operation at program.c:14 by calling function 'create_my_buffer'.

Fixing The Error

To fix a TAINTED_INT warning, we need to change the source so that the value returned from read_data_from_file is checked. The updated source looks like below:

int get_from_file(int handle);
int create_my_buffer(int size);
void send_buffer(int bufHandle);

int handle = 0x700;

int read_data_from_file() {
    int data = get_from_file(handle);
    return data;
}

#define MAX_SIZE 10000

int main() {
    int val = read_data_from_file();

    if (val > 0 && val <= MAX_SIZE) {
        int bufHandle = create_my_buffer(val);

        send_buffer(bufHandle);
    }
    return 0;
}

Since the source code is changed, we have to rebuild the file before the final analysis like below:

$ svace build ./build_all.sh
$ svace analyze

Tutorial for Go

This chapter contains an example of using Svace function specifications for a simple Go program. It works both Linux and Windows distribs.

All public Go specfunctions are contained in the
svace/specifications/go-include/public_specfunc/public_specfunc.go file.

In order to write specifications, package with public specfunctions must be used as external Go module in user project. User can write specifications for their library using specfunctions. The package import path of the user library package and specification package must be similar. Svace specifications work only in module aware mode. You can find more info via this link.

An Example Program

> cat go.mod
module go-include

go 1.20

> cat go.mod
module my/code

go 1.20

require go-include v0.0.0
replace go-include v0.0.0 => ../go-include

> cat go.mod

module my/code

go 1.20

Note: Svace matches a specification and a modeled function via function name, argument number and package import path. Therefore you need to remeber than import path of package with specification and package from your project must be the same. In this example, user module has the following module name: my/code and import path for user/leak/ package is my/code/leak. The folder with specification contains go.mod with the following module name: my/code and import path for spec/leak/ package is my/code/leak. Both import path are the same.

// file user/leak/custom_spec.go 
package leak

import "os"

type MyFile struct {
    file *os.File
}

// a user function that returns a resource
func My_Open(path string) (*MyFile,error) {
    var mf *MyFile
    var err error
    return mf,err
}

func (mf *MyFile) Dosomething()  {
}

// a user function that closes a resource
func (mf *MyFile) Close() {
    mf.file.Close()
}

// file user/test_custom.go 
package user

import "my/code/leak"

func test1(path string) {
    mf, err := leak.My_Open(path) //svace: emitted HANDLE_LEAK
    if err != nil {
        return
    }
    mf.Dosomething()
}

To build project which contains go.mod you need to build it in module directory. You can’t build Go project outside module directory. The build script:

$ cat  build_all.sh
#!/bin/bash
cd user/
go build test_custom.go

$ svace init
$ svace build ./build_all.sh
$ svace analyze

Svace won’t find HANDLE_LEAK vulnerability. The reason for it is that Svace doesn’t have any information about functions my/code/leak.My_Open and my/code/leak.MyFile.Close().

Using Specifications

To provide information about user libraries we have to add Svace specifications. The custom_spec.go file with specifications is like the following:

// file spec/leak/custom_spec.go 
package leak

import "os"
import . "go-include/public_specfunc"

type MyFile struct {
    file *os.File
}

func My_Open(path string) (*MyFile,error) {
    var mf *MyFile
    var err error
    Sf_overwrite(&mf)
    Sf_overwrite(&err)
    Sf_handle_acquire(mf, 0)
    return mf,err
}

func (mf *MyFile) Close()  {
    mf.file.Close()
    Sf_handle_release(mf, 0)
}

$ svace spec add --local spec/leak/custom_spec.go

$ svace analyze

HANDLE_LEAK: The handle mf was created at custom-spec.go:14 by calling function leak.My_Open at test_custom.go:6 and lost at  test_custom.go:11.

Fixing The Error

To fix a HANDLE_LEAK warning, we need to add call of my/code/leak.MyFile.Close() function. The updated source looks like below:

// file user/test_custom.go 
package user

import "my/code/leak"

func test1(path string) {
    mf, err := leak.My_Open(path) //svace: not_emitted HANDLE_LEAK
    if err != nil {
        return
    }
    mf.Dosomething()
    mf.Close()
}

Since the source code is changed, we have to rebuild the file before the final analysis like below:

$ svace build ./build_all.sh
$ svace analyze

C/C++ Specifications

C/C++ specifications are functions written in C/C++. Those functions are analyzed by Svace the same way as any other functions. During analysis summaries of specifications will be used instead of summaries of analyzed functions. For describing function or parameter properties special Svace functions can be called in the specification. Such functions are called specfunctions. Spec functions are prefixed with sf_ and have a special meaning for Svace.

All public specfunctions are contained in the
svace/specifications/include/public-specfunc.h file. Svace internal specifications may use other internal specfunctions that are not advisable for public use.

Common Specifications

Svace doesn’t have a specfunction to denote an argument dereference. It is enough to dereference a variable in the specification source.

void foo(int*a) {
    int val = *a;//parameter a is dereferenced
}

void bar(int**b) {
    int val = **b;//parameter b is dereferenced 
                  //and (*b) is also dereferenced.
}

If parameter is dereferenced under some condition then the condition can be written as is in the source code:

void foo(int*a, int flag) {
    if (flag > 0) {
        int val = *a;//parameter a is dereferenced if flag > 0
    }
}

The same technique may be used for other properties. E.g., to denote a buffer access, a specification has to contain a code with buffer access:

void access(char* buf, int index) {
    char ch = buf[index];
}

It is possible to denote other properties. The exact number of those varies between Svace versions.

int ret(char* buf, int index) {
    return index;
}

int ret(int index) {
    if (index < 0) return -1;
    return 1;
}

void fill(int* p, int val) {
    *p = val;
}

Execution Terminations

The sf_terminate_path specfunction denotes that the current execution path is terminated (with calling exit-like functions, an infinite loop or crashes).

void exit(int code) {
    sf_terminate_path();
}

void error(int status, int errnum, const char *fmt, ...) {
    sf_use_format(fmt);

    if (status > 0)
        sf_terminate_path();
}

The first specification for exit states that the exit function never returns. The second specification for error states that this function does not return only when the status variable is positive.

Overwrite Specifications

Those specifications show that the pointed memory has been assigned with some value. There are two ways of using this specification.

First, it is useful for denoting that a memory reachable via a pointer is overwritten by the modeled function:

double modf(double x, double *iptr) {
    sf_overwrite(iptr);
}

Now Svace knows that the memory pointed to by iptr is assigned with the new value when the modf function is called.

The second way of using such a specification is for describing new variables. By default Svace assumes that every variable is not initialized. Therefore the following code is incorrect:

double modf(double x, double *iptr) {
    double ret;
    return ret;
}

This specification tells Svace that the modf function returns an uninitialized value, which was likely not intended. For the correct specification it is needed to add a call to sf_overwite:

double modf(double x, double *iptr) {
    double ret;
    sf_overwrite(&ret);//note: `&` is very important here
    return ret;
}

Note that sf_overwrite takes an address of the memory being initialized and not the memory itself.

double modf(double x, double *iptr) {
    sf_overwrite(iptr);
    
    double ret;
    sf_overwrite(&ret);
    return ret;
}

The sf_overwrite_int_as_ptr companion function is needed for cases when a pointer is naked (the pointed type is unknown or irrelevant).

For most specfunctions their calling order is not important, but for the sf_overwrite functions the order is significant. Changing the calling order will change the specification meaning as shown below.

//incorrect specification
ssize_t recv(int s, void *buf, size_t len, int flags) {
    ssize_t res;
    sf_set_possible_negative(res);
    sf_overwrite(&res);
    return res;
}

In this example below the uninitilized value of variable res is marked as possibly negative. But after the call of sf_overwrite the variable is assigned the new value which is unknown (not negative). The correct specifications looks like the following:

ssize_t recv(int s, void *buf, size_t len, int flags) {
    ssize_t res;
    sf_overwrite(&res);
    sf_set_possible_negative(res);
    return res;
}

Working with Resources

Acquire and release specfunctions

sf_handle_acquire asserts that the ptr pointer points to the newly created resource (e.g. a file).

sf_handle_acquire_int_as_ptr has the same meaning but is used for resources which are represented in the C code as integers (handles).

sf_handle_release asserts that the handle represented by ptr was closed or the corresponding resource was released.

The category parameter is used for specifying the created resource type. The following values are supported:

#define MALLOC_CATEGORY     100
#define KMALLOC_CATEGORY    102
#define VMALLOC_CATEGORY    102
#define NEW_CATEGORY        200
#define NEW_ARRAY_CATEGORY  300
#define BSTR_ALLOC_CATEGORY 400

#define SOCKET_CATEGORY         1200
#define FILE_CATEGORY           1300
#define HANDLE_FILE_CATEGORY    1400
#define DIR_CATEGORY            1500
#define DL_CATEGORY             1600
#define MMAP_CATEGORY           2000
#define GETADDRINFO_CATEGORY    2100

#define X11_DEVICE              3001
#define X11_CATEGORY            3002

#define SQLITE3_NONFREEABLE_CATEGORY   4000
#define SQLITE3_DB_CATEGORY            4001
#define SQLITE3_MALLOC_CATEGORY        4002
#define SQLITE3_TABLE_CATEGORY         4003
#define SQLITE3_STMT_CATEGORY          4004
#define SQLITE3_BLOB_CATEGORY          4005
#define SQLITE3_VALUE_CATEGORY         4006
#define SQLITE3_MUTEX_CATEGORY         4007
#define SQLITE3_BACKUP_CATEGORY        4008
#define SQLITE3_SNAPSHOT_CATEGORY      4011

The values between 0 and 10000 are reserved for internal use in Svace. All user resource categories must have values greater than 10000. The categories are needed for finding errors when a resource is created by one function but released with inappropriate function.

FILE *fopen(const char *filename, const char *mode) {
    FILE *res;
    sf_overwrite(&res);//res is initialized
    sf_overwrite(res);//pointed memory is also initialized
    sf_handle_acquire(res, FILE_CATEGORY);
    return res;
}

int fclose(FILE *stream) {
    sf_handle_release(stream, FILE_CATEGORY);
}

Svace has two types of warnings for resource leaks. The first is called MEMORY_LEAK and the second is called HANDLE_LEAK. The above functions have the same meaning as their handle counterparts. However, when Svace finds a resource leak, with those specifications it will emit a warning of type MEMORY_LEAK instead of HANDLE_LEAK. Also, Svace handles null values differently: if a pointer is null than the memory is not acquired; for HANDLE_LEAK groups zero handles are assumed being legal handles for acquired resources.

Svace has special warnings type for the strdup function return value. For denoting that a function returns a strdup result, Svace has the sf_strdup_res specfunction. It has the same semantic as sf_new.

#define WINDOW_HANDLE_CATEGORY 20001
#define DB_HANDLE_CATEGORY 20002

//create new window
int createWindow(const char *id) {
    int res;
    sf_overwrite(&res);
    sf_overwrite(res);
    sf_handle_acquire(res, WINDOW_HANDLE_CATEGORY);
    return res;
}

//destroy window with the given handle
void closeWindow(int handle) {
    sf_handle_release(handle, WINDOW_HANDLE_CATEGORY);
}

//create new data base connection
int createDB(const char *path, const char*login) {
    int res;
    sf_overwrite(&res);
    sf_overwrite(res);
    sf_handle_acquire(res, DB_HANDLE_CATEGORY);
    return res;
}

//destroy connection with the given handle
void closeDB(int handle) {
    sf_handle_release(handle, DB_HANDLE_CATEGORY);
}

Now Svace knows that functions createWindow and createDB create resources of corresponding types and the closeWindow and closeDB functions release them. As a result, in the following code Svace finds a resource leak:

int createIf(const char *id, const char* flags) {
    int handle = createWindow(id);
    
    if (flags < 0)//here is error: closeWindow is not called
        return ERROR;
        
    return handle;
}

void readDB(const char *id) {
    int handle = createDB(id, "admin");
    
    readDBImpl(handle);
    
    closeWindow(handle);//error - handle is not for window resources.
}

Conditional acquire

Many resource acquire functions return an error code when a memory or a resource were not created. The above functions are used for modeling such situations.

The sf_not_acquire_if_eq specfunction marks that the memory pointed to by pval was not created if var = code. The
sf_not_acquire_if_eq_int_as_ptr specfunction does the same for handles.

The sf_not_acquire_if_less specfunction marks that the memory pointed to by pval was not created if var < val. The
sf_not_acquire_if_less_int_as_ptr specfunction does the same but handles.

The sf_not_acquire_if_greater specfunction marks that the memory pointed to by pval was not created if var > val. The
sf_not_acquire_if_greater_int_as_ptr specfunction does the same for handles.

FILE *fopen(const char *filename, const char *mode) {
    FILE *res;
    sf_overwrite(&res);
    sf_overwrite(res);
    sf_handle_acquire(res, FILE_CATEGORY);
    sf_not_acquire_if_eq(res, res, 0);
    return res;
}

This specification says that the fopen function creates a resource and this resource is not created if it equals to null. Note that calling sf_handle_acquire is still needed: the call of sf_not_acquire_if_eq doesn’t state that a resource is created.

int asprintf(char **ret, const char *format, ...) {
    sf_overwrite(ret);
    sf_overwrite(*ret);
    sf_new(*ret, MALLOC_CATEGORY);

    int res;
    sf_not_acquire_if_less(*ret, res, 1);
    return res;
}

For the asprintf function specification Svace gets information that the new memory is created and the pointer to this memory is written to the memory pointed to by the first parameter. In case of failure the return value will be less that 1.

int open(const char *name, int flags, ...) {
    int x;
    sf_overwrite(&x);
    sf_overwrite_int_as_ptr(x);
    sf_handle_acquire_int_as_ptr(x, HANDLE_FILE_CATEGORY);
    sf_not_acquire_if_less_int_as_ptr(x, x, 3);
    return x;
}

This specification says that the open function creates the new resource. If it is less than 3 than it was not created. The original open function returns -1 in case of error, but in real code it is common to check the return value to be positive. That’s why we didn’t use the sf_not_acquire_if_eq_int_as_ptr specfunction. 0, 1, and 2 are used for stdin, stdout, and stderr, respectively. It is not necessary to release those handles. That’s why the last argument of sf_not_acquire_if_less_int_as_ptr is 3.

Memory management specifications

The sf_invalid_pointer specfunction marks that its second argument p is invalid when it is not equal to the first argument, newp. It is used for modeling the realloc function:

void *realloc(void *ptr, size_t size) {
    void *retptr;
    sf_overwrite(&retptr);
    sf_overwrite(retptr);
    sf_new(retptr, MALLOC_CATEGORY);
    sf_invalid_pointer(ptr, retptr);
    return retptr;
}

From this specification Svace knows that realloc creates the new memory and returns a pointer to it. If the new memory is not equal to the first argument, than the result is invalid and cannot be used.

The sf_escape specfunction denotes that the memory pointed to by pval is escaped. Now the pointer itself and all referenced values (the memory reachable via this pointer) can be saved in a variable or deleted. Svace won’t emit memory leak warnings for all these values.

int putenv(char *cmd) {
    sf_escape(cmd);
}

The putenv function stores its parameter internally. So for the following code Svace does not emit leak warnings:

putenv(strdup(var));

Tainted Specifications

Most tainted checkers are written as source-sink checkers. A source is a function that gets its data from external environment (a file, user input, network and etc.). A sink is a vulnerable operation where the source data should not be used. Sanitization is a process of checking or correcting the source data so it becomes safe for further usage.

Svace always treats array accesses as vulnerable operations for tainted integer indexes.

Sources of tainted values

The sf_set_tainted specfunction marks its string argument as tainted which means the following:

char *gets(char *s) {
    sf_overwrite(s);
    sf_set_tainted(s);
    
    char *str;
    sf_overwrite(&str);
    sf_set_tainted(str);
    return str;
}

The sf_set_tainted_int specfunction indicates that its integer argument is tainted. It may have any values. The sf_set_tainted_char specfunction has the same meaning for the 8-bit character type.

uint32_t htonl(uint32_t hostlong) {
    uint32_t res;
    sf_overwrite(&res);
    sf_set_tainted_int(res);
    return res;
}

The sf_set_tainted_interval specfunction indicates that its first parameter is tainted and has values inside the [lower;upper] interval, i.e. lower ≤ i ≤ upper. The interval bounds lower and upper can be set by integer literals or variables available within the scope of sf_set_tainted_interval call. Additionally, if exclusive bounds relative to some variable var need be specified, i.e. i > var or i < var, one can use var + 1 for lower bound and var − 1 for upper bound.

Specification in the example below shows that fgets function returns a character value or -1 (in case of error).

int fgetc(FILE *stream) {
    int res;
    sf_overwrite(&res);
    sf_set_tainted_interval(res, -1, 255);
    return res;
}

The following example demonstrates usage of sf_set_tainted_interval specfunction to model exclusive bound on return value. Suppose we have a function randomInt which returns integer values i such that a ≤ i < b where a and b are integer parameters of that function. The specification of this function would be as follows:

int randomInt(int a, int b) {
    int res;
    sf_overwrite(&res);
    sf_set_tainted_interval(res, a, b-1);
    return res;
}

The sf_set_tainted_buf specfunction marks the memory pointed to by ptr as tainted. The memory size (number of tainted bytes) is (size + shift). If size is zero that there is no limit. The shift parameter is a constant difference between the size limit and the maximum string length (0 for most functions, -1 for fgets).

char *fgets(char *s, int num, FILE *stream) {
    sf_overwrite(s);
    sf_set_tainted(s);
    sf_set_tainted_buf(s, num, -1);

    char *str = s;
    return str;
}

In this specification Svace treats num bytes pointed to by the modeled function return value as tainted.

Converting functions

The sf_str_to_int specfunction indicates that i is an integer representation of str string content. The sf_str_to_long specfunction does the same for long values.

Currently Svace uses a heuristic that if a program converts a string to integer, then the conversion result is tainted. In most cases arguments of those functions are tainted.

int atoi(const char *arg) {
    int res;
    sf_overwrite(&res);
    sf_str_to_int(arg, res);
    return res;
}

Transferring taintedness

The sf_transfer_tainted specfunction marks len bytes of the first parameter, dst, as tainted when the second parameter, src, is tainted. The example usage is below.

void *memcpy(void *dst, const void *src, size_t num) {
    sf_transfer_tainted(dst, src, num);

    return dst;
}

Sinks for tainted values

The sf_set_trusted_sink_int specfunction indicates that the i parameter is used in a vulnerable operation. Its bounds have to be checked for some values. It is possible to check values by comparing with other variable.

int gettainted() {
    int tainted_res;
    sf_overwrite(&tainted_res);
    sf_set_tainted_int(tainted_res);
    return tainted_res;
}

int trusted(int c) {
    sf_set_trusted_sink_int(c);
}

void error() {
    int index = gettainted();

    //Svace emits a warning that 'index' bounds are not checked
    trusted(index);
}

void errorToo() {
    int index = gettainted();

    if (index > 10) 
        return;
        
    //Svace emits a warning that the lower bound is not checked
    trusted(index);
}

void noError() {
    int index = gettainted();

    if (index < 0 || index > 10) 
        return;
        
    //no warnings, both lower and upper bounds are checked
    trusted(index);
}

void compareWithVar(int limit) {
    int index = gettainted();

    if (index < 0 || index > limit) 
        return;
        
    //no warnings, both lower and upper bounds are checked
    trusted(index);
}

Another example of using sf_set_trusted_sink_int is in the malloc specification:

void *malloc(size_t size) {
    sf_set_trusted_sink_int(size);
}

This code says that the malloc parameter that comes from external sources has to be checked for bounds. Svace doesn’t find exact bound limits because they are application specific.

The sf_set_trusted_sink_char specfunction has the same meaning for character type. The only difference that instead of emitting a warning of type TAINTED_INT Svace will emit its subtype called TAINTED_INT.CTYPE.

The sf_set_trusted_sink_ptr specfunction states that its string argument is used in a vulnerable operation. It shouldn’t get tainted strings.

int execl(const char *path, const char *arg0, ...) {
    sf_tocttou_access(path);
    sf_set_trusted_sink_ptr(path);
    sf_fun_does_not_update_vargs(2);
    // The exec* functions return only if an error has occurred.
    int res;
    sf_set_errno_if(res, sf_top());
    sf_no_errno_if(res, sf_bottom());
    return res;
}

The sf_use_format specfunction indicates that its argument is a printf-like format string. It shouldn’t get tainted arguments.

int fprintf(FILE *stream, const char *format, ...) {
    sf_use_format(format);
}

Sanitization

The sf_sanitize specfunction removes the tainted mark from its arguments. It can be used in the following cases:

int strcmp(const char *s1, const char *s2) {
    sf_sanitize(s1);
    sf_sanitize(s2);
}

The above specification just removes the tainted mark from strcmp arguments as Svace considers this call an evidence of sanitization.

Buffers and Strings

Buffers

The sf_buf_size_limit specfunction shows that the ptr parameter may be used to access a buffer with offsets [0, size). Unless sf_buf_stop_at_null (see Nonterminated strings) is used, the access doesn’t stop at null terminators.

The sf_buf_size_limit_read specfunction has the similar meaning as
sf_buf_size_limit but the buffer access is read-only.

char *fgets(char *s, int num, FILE *stream) {
    sf_overwrite(s);
    sf_buf_size_limit(s, num);

    char *str = s;
    return str;
}

int snprintf(char *str, size_t size, const char *format, ...) {
    sf_bitinit(str);
    sf_buf_size_limit(str, size);
}

char *strncat(char *s, const char *append, size_t count) {
    sf_buf_size_limit_read(append, count);
    sf_buf_stop_at_null(append);
}

The specification says that the strncat function stops reading the append string where it contains null.

The sf_buf_size_limit_strict specfunction specifies that limit parameter must be withing buffer bounds. If Svace defines size of buffer and won’t be able to define value of parameter than the warning is emitted.

errno_t memcpy_s(void *dst, size_t dstSize,
                 const void *src, size_t num) {
    sf_buf_size_limit_strict(dst, dstSize);
    sf_buf_size_limit(src, num);
    
    errno_t res;
    sf_overwrite(&res);
    return res;
}

The specification above says that parameter src is limited by parameter num and parameter dst is limited by parameter dstSize. The difference is in Svace behavior for cases where buffer size is known and parameter values are not known. In this case Svace emits warning only for parameter dst. For parameter src a warning will be emitted only if Svace defined that parameter’s value leads to overflow.

Nonterminated strings

The sf_buf_stop_at_null specfunction says that the pointer is used to access a string until a null byte is encountered. Unless sf_buf_size_limit (see Buffers) is used, the access stops only at a null byte.

int atoi(const char *arg) {
    sf_buf_stop_at_null(arg);
}

The sf_set_possible_nnts specfunction shows that dst can become a nonterminated string. Such values are handled by Svace as a source of nonterminated string errors.

ssize_t recv(int s, void *buf, size_t len, int flags) {
    sf_overwrite(buf);
    sf_set_possible_nnts(buf);
    sf_bitinit(buf);
}

Modeling strlen functions

The sf_strlen specfunction denotes that len, the first parameter, is a length of the C string str. The sf_wcslen specfunction does the same for wide strings.

size_t strlen(const char *s) {
    size_t res;
    sf_overwrite(&res);
    sf_strlen(res, s);
    return res;
}

Value properties

Negative values

The sf_set_possible_negative specfunction states that its parameter may have a negative value. It has to be checked before accessing buffers and using in functions that don’t expect negative values.

int putchar(int c) {
    int ret;
    sf_overwrite(&ret);
    sf_set_possible_negative(ret);
    return ret;
}

The sf_set_must_be_positive specfunction states that its parameter can’t be negative. Zero is accepted.

int dup(int oldd) {
    sf_set_must_be_positive(oldd);
}

Function results

The sf_no_check_return specfunction specifies that its argument, which must be the return value of a function, will not be processed by a checkers that finds unchecked function return value using statistics.

The function description below shows an example of a function for which the UNCHECKED_FUNC_RES.STAT checker will not collect statistics of checking its return values.

The sf_must_be_checked specfunction specifies that its argument must be somehow checked by caller function. The argument denotes some error code. Svace dosn’t have any requirements to the checking. It may be compared with any other value.

int munmap(void *addr, size_t len) {
    int res;
    sf_overwrite(&res);
    sf_must_be_checked(res);
    return res;
}

The sf_fread, sf_ferror, sf_feof specfunctions are needed for
the UNCHECKED_FUNC_RES.FREAD checker. The checker emits a warning if the return value of fread-like functions was checked for error but the ferror and feof functions were not called.

size_t fread(void *ptr, size_t size,
             size_t nitems, FILE *stream) {
    size_t res;
    sf_overwrite(&res);
    sf_must_be_checked(res);
    sf_fread(res, stream);
    return res;
}

int feof(FILE *stream) {
    int res;
    sf_overwrite(&res);
    sf_feof(stream);
    return res;
}

int ferror(FILE *stream) {
    sf_ferror(stream);
}

int foo(FILE *pFile, long lSize, char* buffer) {
    int res = fread(buffer, 1, lSize, pFile);
    if (!res) {//error: no ferror and feof
        return 1;
    }
    return 0;
}

int correct(FILE *pFile, long lSize, char* buffer) {
    int res = fread(buffer, 1, lSize, pFile);
    if (!res) {
        if (ferror(pFile))
             printf ("Error!\n");
        return 1;
    }
    return 0;
}

Other Specifications

Initialization

The sf_bitcopy specfunction shows that the memory pointed to by dst is initialized with the content of src.

void *memcpy(void *dst, const void *src, size_t num) {
    sf_bitcopy(dst, src);
}

The sf_bitinit specfunction marks values pointed to by ptr as completely initialized. The sf_deepinit specfunction does the same for all memory that is reachable from ptr. If ptr points to a structure, then all its fields are initialized. If a field is a structure itself or points to a structure, then those fields are also initialized.

void *memset(void *ptr, int value, size_t num) {
    sf_bitinit(ptr);
}

ssize_t recvmsg(int s, struct msghdr *msg, int flags) {
    sf_deepinit(msg);
}

With this specification, the recvmsg function initializes not only the msg parameter itself but also its fields.

Important: do not confuse sf_bitinit and sf_overwrite functions. sf_overwrite shows that the variable changes its value to a completely new one. As a result, the analysis will stop tracking all the previous properties of this variable. The sf_bitinit specfunction only marks the variable as being initialized. It does not affect any other properties, which will remain the same.

void hard_init(void*p) {
    sf_overwrite(p);   
}

void soft_init(void*p) {
    sf_bitinit(p);   
}

int foo() {
    char** p = malloc(sizeof(char*));
    *p = malloc(sizeof(char));
    hard_init(p);
    int ret = **p;
    free(*p);
    free(p);
    return ret;
}

int bar() {
    char** p = malloc(sizeof(char*));
    *p = malloc(sizeof(char));
    soft_init(p);
    int ret = **p;
    free(*p);
    free(p);
    return ret;
}

For the foo function Svace emits a memory leak warning because the value of the p pointer that pointed to headp was overwritten and lost.

int sqlite3_close(sqlite3 *db) {
    return sf_get_some_int();
}

int sqlite3_close(sqlite3 *db) {
    int res;
    sf_overwrite(&res);
    return res;
}

Null pointer dereference

The sf_set_possible_null specfunction marks the pointer as containing null value. It should be checked for being null before dereferencing. The sf_not_null specfunction marks the pointer as non-null. Svace won’t emit dereference warnings for this pointer.

jbooleanArray NewBooleanArray(JNIEnv *env, jsize length) {
    jobject *res;
    sf_overwrite(&res);
    sf_set_possible_null(res);
    return res;
}

Function NewBooleanArray may return null. Its result has to be checked before dereferencing.

Svace doesn’t have a special function for denoting dereferences. As mentioned in Section Common Specifications, to write a specification for a function that dereferences its argument it is enough to add the dereference to the code:

FILE *fdopen(int fildes, const char * mode) {
    char d1 = *mode; //dereference here
}

Lock-unlock

The sf_lock specfunction marks its argument as a locked mutex. The sf_unlock specfunction marks its argument as an unlocked mutex. The sf_trylock specfunction marks its argument as a locked mutex but it doesn’t lead to the DOUBLE_LOCK warning. The mutex will be locked only if it was in the unlocked state. Otherwise nothing will be changed.

These specfunctions are used when writing locking function specifications as shown below.

typedef struct pthread_mutex pthread_mutex_t;
struct pthread_mutex;

int pthread_mutex_lock(pthread_mutex_t *mutex) {
    sf_lock(mutex);
}

int pthread_mutex_unlock(pthread_mutex_t *mutex) {
    sf_unlock(mutex);
}

int pthread_mutex_trylock(pthread_mutex_t *mutex) {
    sf_trylock(mutex);
}

The sf_thread_shared specfunction indicates that the data parameter is used by another thread, as shown below.

struct pthread;
typedef struct pthread pthread_t;

struct pthread_attr;
typedef struct pthread_attr pthread_attr_t;

int pthread_create(pthread_t *thread, const pthread_attr_t *attr,
                   void *(*start_routine) (void *), void *arg) {
    sf_thread_shared(arg);
}

The sf_success_lock_if_zero specfunction associates a variable with the mutex state. If the variable is not zero, then the mutex was not locked. The example can be seen in specifying the pthread_mutex_lock function.

int pthread_mutex_lock(pthread_mutex_t *mutex) {
    sf_lock(mutex);

    int res;
    sf_overwrite(&res);
    sf_success_lock_if_zero(res, mutex);
    return res;
}

Other concurrency specifications

The sf_long_time specification marks the caller function as a function which may be executed for a long time. Locking such function may lead to the performance degradation. The examples can be seen below.

int listen(int sockfd, int backlog) {
    sf_long_time();
    
    int res;
    sf_overwrite(&res);
    sf_set_possible_negative(res);
    return res;
}

unsigned int sleep(unsigned int ms) {
    sf_long_time();
}

Variable argument functions

The sf_fun_does_not_update_vargs and sf_fun_updates_vargs specfunctions are needed for modeling functions with variable arguments number. The sf_fun_does_not_update_vargs specfunction states that the caller function doesn’t update its arguments starting from from meaning that the following arguments are read only. Its counterpart sf_fun_updates_vargs states that the caller function changes its arguments from the specified number from, so after calling such a function the passed arguments are initialized.

int fprintf(FILE *stream, const char *format, ...) {
    sf_fun_does_not_update_vargs(2);
}

int fscanf(FILE *stream, const char *format, ...) {
    char derefStream = *((char *)stream);
    char d1 = *format;
    sf_use_format(format);
    
    sf_fun_updates_vargs(2);
}

Vulnerable functions

The above specfunctions are used when there is a need to deprecate some functions. For most of them Svace doesn’t do any complicated analysis but just emits a warning when the modeled function was called.

The sf_vulnerable_fun specfunction marks the caller function as vulnerable which shouldn’t be used. This specfunction may be used for any deprecated function. For those functions Svace emits the PROC_USE.VULNERABLE warning. The sf_vulnerable_fun_temp specfunction does the same but the emitted warning type is PROC_USE.VULNERABLE.TEMP, as shown below.

char *strcat(char *s, const char *append) {
    sf_vulnerable_fun("This function is unsafe,"
        " use strncat instead.");
}

char *tempnam(const char *dir, const char *pfx) {
    sf_vulnerable_fun_temp("This function is susceptible "
    "to a race condition occurring between "
    "selection of the file name and creation "
    "of the file, which allows malicious "
    "users to potentially overwrite "
    "arbitrary files in the system. "
    "Use mkstemp(), mkstemps(), or mkdtemp() instead.");
}

The sf_fun_rand specfunction is the same as sf_vulnerable_fun but Svace emits the PROC_USE.RAND warning.

The sf_fun_rand specfunction is the same as sf_vulnerable_fun_sscanf but Svace emits the PROC_USE.VULNERABLE.SSCANF warning, as shown below.

int rand(void) {
    int res;
    sf_overwrite(&res);
    sf_set_values(res, 0, 32767);//use RAND_MAX?
    sf_fun_rand();
    return res;
}

The sf_vulnerable_fun_type specfunction allows setting the suffix for the emitted warning, as shown below for the getenv function specification.

char *getenv(const char *key) {
    sf_vulnerable_fun_type("getenv return value is untrusted",
                           "GETENV");
}

Now when the call to getenv is detected, Svace emits the
PROC_USE.VULNERABLE.GETENV warning.

Note: for some cases where Svace can discover that the function call is safe it won’t emit the warning. For example:

void foo(char*buf) {
    int x;
    char str[10];
    sscanf(buf, "%d%5s", &x, str);
}

In this code the sscanf functiion fills only 5 bytes in the str string. Since its size is 10 it won’t lead to any errors.

sprintf, scanf-like functions

The sf_fun_sprintf_like specfunction denotes that the caller function is a sprintf-like function meaning that it behaves in a similar fashion.

The sf_fun_scanf_like specfunction denotes that the caller function is a scanf-like function. Its parameter is the format string argument index (starting from 0).

The sf_fun_printf_like specfunction denotes that the caller function is a printf-like function. Its parameter is the format string argument index (starting from 0).

int sprintf(char *s, const char *format, ...) {
    sf_fun_sprintf_like();
}

int sscanf(const char *s, const char *format, ...) {
    sf_fun_scanf_like(1);
    sf_fun_updates_vargs(2);
}

int fprintf(FILE *stream, const char *format, ...) {
    sf_fun_printf_like(1);
    sf_fun_does_not_update_vargs(2);
}

Sensitive data leaks

The sf_sec_leak specfunction says that the data from the data buffer of size size is saved to the external memory and may be leaked.

Exceptions

The sf_could_throw specfunction indicates that the caller function may throw an exception. This exception should be caught in the analyzed program. The sf_could_throw_pedantic specfunction has the similar meaning but if the program doesn’t catch an exception, Svace emits warning with lower priority. Both functions have an argument, which is the exception name. Svace will compare the name with the names of types used in catch statements.

Combining Values

The above specfunctions offer a flexible way of specifying restrictions on integer values as well as other conditions. All functions return a value which has the specified properties. It may be used in other specifications.

The sf_range specfunction creates an integer variable which value lies inside the [left;right] range, as in the example below.

int x = sf_range(1, 10);
//Now variable x has values between 1 and 10.

The sf_cond_range specfunction creates an integer variable which has the value restricted by a condition. Its first argument can have the following values: ">", "<", ">=", "<=", and "==". The example is shown below.

int x = sf_cond_range(">", 7);
//Now variable x has values more than 7

The sf_cond specfunction associates a condition with the return value as follows: left cond right where cond can have the following values: ">", "<", ">=", "<=", "==", and "!=". Left and right can be either constants and variables. In the below specification sf_cond(a, ">", 0) associates the a > 0 condition with the return value stored in cond.

void foo(int a, int b, int c) {
    int cond = sf_cond(a, ">", 0);
    if (cond)
        return b;
    return c;
}

The sf_join and sf_meet specfunctions allow combining results of other functions listed here: sf_join joins values of its arguments, while sf_meet intersects values of its arguments.

void foo(int a, int b, int c) {
    int c1 = sf_cond(a, ">", 0);
    int c2 = sf_cond(b, ">=", c);
    int c3 = sf_cond(c, "<", 10);
    
    int join = sf_join(c1, c2);
    int meet = sf_meet(join, c3);
    if (meet)
        return 0;
    return c;
}

Specification for user checkers

Svace allows to register simple checkers for checking function arguments. Those checkers verify properties of function arguments.

Language of creation new checker is declarative. Specifications set up what Svace should find and didn’t tell how to find. Svace may use different analysis for finding specified error and different Svace version may implement it different ways.

Range checkers

The sf_check_int_arg create new checker for checking range of argument arg. The checker will emit warning if specified function will be called with arguments that is outside of range. Spec-function sf_cond_range should be used for specifing range.

The example of creation new checker for verifying that function argument is positive.

void set_up_name(int id, char *name) {
    sf_check_int_arg(
            id,
            sf_cond_range(">", 0),
            "NOT_POSITIVE",
            "Id-parameter must be positive.");
}

The specification above register checker. The checker will be verify range of first parameter for function set_up_name. In case if parameter may have non-positive values Svace would emit a warning of type USER.ARG_RANGE.

void foo() {
    set_up_name(0, "admin"); //error: id is not positive
    
    set_up_name(1, "user1"); //all ok
}

Svace will be used additional analysis for detecting values of variables. Example of cases where the warning will be emitted:

void const_use() {
    int id = 0;
    set_up_name(id, "admin"); //error will be emitted
}

void compare(int id) {
    if (id<0)
        set_up_name(id, "admin"); //error will be emitted too
}

void bar(int id) {
    set_up_name(id, "admin"); //no warning
}

The reason that we don’t know where parameter of function bar is used. Future Svace versions may propagate information to function bar and than check that argument of bar is positive.

Constant checkers

Spec-functions sf_not_constant and sf_constant may be used as second argument of spec-function sf_check_int_arg as range. Function sf_not_constant means that parameter mustn’t be a constant and function sf_constant means that parameter must be a constant.

void set_up_level(int id, int level) {
    sf_check_int_arg(
            level,
            sf_constant(),
            "NOT_A_CONSTANT",
            "Parameter level must be a constant.");
}

void set_up_age(int id, int ge
    sf_check_int_arg(
            age,
            sf_not_constant(),
            "CONSTANT_USE",
            "Parameter age mustn't be a constant.");
}

Specifications above create two checkers. First checker for function set_up_level will check that actual parameter is constant. Second checker for function set_up_age will check that actual parameter is not constant. In case of rule violation Svace will emit warning of type USER.ARG_RANGE.

void foo(int id, int x) {
    set_up_level(id, x); //error - not a constant
    
    set_up_age(id, 18); //error - constant use
    
    int age = 22;
    set_up_age(id, age); //error again
}

void bar(int id, int x) {
    set_up_level(id, 3); //all ok
    
    set_up_age(id, x); //all ok
}

Guard checkers

Spec-function sf_add_args_guard creates a flexible rule for function arguments. It has a predicate of type boolean that will be applied for actual function arguments. Only simple cases of guards are allowed. If guard is violated thatn Svace will emit warning of type USER.ARG_GUARD.

void my_mod(int a, int b) {
    sf_add_args_guard(
        a > b,
        "NOT_SMALLER",
        "First parameter must be smaller than the second one.");
}

void bar(int a) {
    my_mod(10, 15); //all ok, 10 < 15
    
    my_mod(20, 15); //error
    
    my_mod(a, 15); //no warning, not enough information
}

void hasMask(int arg) {
    sf_add_args_guard(
            (arg & 0x07) == 0x07,
            "NO_MASK",
            "Parameter must have mask 0x07.");
}

The specification above will create checker for verifying that argument has bitmask 0x07 which mean that all those bits are set up.

void bar(int a) {
    hasMask(a); //no warning
    
    hasMask(0x07); //all ok
    
    hasMask(0x06); //error - not all bits are set up
    
    hasMask(0x227); //all ok
}

Java/Kotlin specifications

Java/Kotlin specifications are classes and their described methods. Those classes are analyzed by Svace the same way as any other classes. During analysis summaries of specifications will be used instead of summaries of analyzed classes.

For describing function or parameter properties special Svace functions can be used in the specification. Such functions are called specfunctions. Specfunctions are static functions of class ‘ru.isp.svace.sf.SpecFunc’ prefixed with sf_ and have a special meaning for Svace.

Another way to describe function behaviour or some usage agreement in Java/Kotlin is to use special annotations. They have no specific naming, but also have special meaning for Svace.

Public specfunctions and annotations are located in the directory
svace/specifications/java-include/ru/isp/svace/sf. Specfunctions are described in SpecFunc.java. Annotations has their own .java files in the same directory.

Class hierarchy

Overridden methods

Annotation ‘@OverriderMustCallSuper’ asserts that overriding method will call superclass method. Therefore, overriding annotated method and NOT calling superclass method is considered as an error.

Context specification

Context specification is a mechanism to specify context in which particular function must be analyzed by Svace. For example, it is possible to specify that some function parameter is tainted or belong to particular interval.

Overview

Svace context specifications have the same format as regular specifications (Specifications Overview). Context specification is written as a function in the same language and with the same declaration as the modeled function. Svace analyzes the specification source code and create special call context for specifying functions. Those functions will be analyzed again with created call context.

void user_function(char*input, int val) {
    sf_set_tainted(input);
    sf_set_possible_negative(val);
}

specifies that function user_function should be analyzed with selected properties of arguments.

Tutorial

This chapter contains an example of using Svace context specifications for a simple program.

An Example Program

void function_to_customize(char*par, int n) { 
    par[10] = 0;

    if (par != 0)
        *par = 'a';
}

$ svace init
$ svace build gcc -c example.c
$ svace analyze

Svace will find error NULL_AFTER_DEREF about inconsistency of using parameter par.

Using Specifications

For doing it we have to create file with another definition of function function_to_customize.

void sf_set_tainted(void*f);

void function_to_customize(char*p, int n) {
    sf_set_tainted(p);
}

$ svace context-spec add --local my-context-spec.c

$ svace analyze

Svace will emit warning TAINTED_PTR.OVERFLOW which mean that length of parameter par is not controlled by user and operation par[10] may lead to buffer overflow.

C/C++ Attributes

Regular attributes

C++ has attribute noreturn to indicate that some function does not return. It indicates that the function will not return control flow to the calling function after it finishes (e.g. functions that terminate the application, throw exceptions, loop indefinitely, etc.).

In the follow code attribute noreturn indicates that function customAssert does not return. Function foo checks a pointer b and calls function customAssert in case if the pointer has null value. Thus, at line (*) pointer b definitely does not have a null value.

void customAssert() __attribute__((noreturn));

int foo(int *b) {
  if (!b)
    customAssert();
  return *b; //(*)
}

Svace takes into account meaning if this attribute. In the above example, warning DEREF_AFTER_NULL will not be emitted because function customAssert has noreturn attribute.

[[noreturn]] void customAssert();

Svace function attributes

Attribute value_interval

Attribute value_interval sets up possible interval range for integer values. It is applied to function return value. The analyzer assumes that specified integer value can not have value outside of this interval during program execution.

int foo(int a);

__attribute__((svace_value_interval(-3, -1))) int foo1(int count) {
    return foo(count);
}

void use(int val) {
    char buf[9];
    buf[val];
}

void example(int x) {
    int y = foo1(x);
    use(y); //NEGATIVE_CODE_ERROR
}

In the above example, attribute value_interval denotes that function foo1 can returns values in interval [-3;-1], e.g. -3, -2 or -1. All such negative values can not be used as array indexes. That is why Svace emits warning NEGATIVE_CODE_ERROR for this code.

Attribute possible_negative

Attribute possible_negative marks functions, which result must be checked for negative values.

int foo(int c);

__attribute__((svace_possible_negative)) int getNeg(){
    int a;
    return foo(a);
}

void example(int b){
    char buf[10];
    int a = getNeg();
    buf[a]=0;//NEGATIVE_CODE_ERROR
}

Svace will emit an error if such value will be used in operation, which does not allow negative values.

Atribute taint_int

Attribute taint_int marks function return value as tainted, which mean that this value is got from external resources and potentially can be controlled by an intruder. Such values must be checked before usage.

int foo(int c);

__attribute__((svace_taint_int)) int badSource(int count) {
    return foo(count);
}

void example(int a) {
    int v = badSource(a);
    sleep(v); //TAINTED_INT
}

In the above code value from badSource is passed to function sleep. If badSource returns too big value, then the program will be paused for too long.

This attributes has another form, which restricts potential range of possible values (the same way as value_interval).

int foo(int c);

__attribute__((svace_taint_int(0, 10))) int badSource(int count) {
    return foo(count);
}

void error_example(int a) {
    char buf[10];
    int v = badSource(a);
    buf[v] = 0; //error TAINTED_INT
}

void no_error(int a) {
    char buf[11];
    int v = badSource(a);
    buf[v] = 0; //all ok
}

In the example above function badSource returns tainted value, but this value is restricted to interval [0;10]. Thus, function error_example has error in case if integer v gets value 10, and function no_error does not have error, because all those values maybe used as indexes for array with size 11.

Atribute taint

Attribute taint marks function return value for strings as tainted, which mean that this value is got from external resources and potentially can be controlled by an intruder. Such values must be checked before usage.

char* impl(char* c);

__attribute__((svace_taint)) char* custom_getenv(char* name) {
    return impl(name);
}

char buf[100];

void test() {
    char* env = custom_getenv("VAR3");

    // Copying a string of unbounded size to a fixed-size buffer.
    strcpy(buf, env);//TAINTED_PTR
}

In the wxample above function custom_getenv can return tainted string. It is length may be controled by and intruder. If it will more than size of buffer buf, then execution of strcpy will lead to an error. Svace emits warning TAINTED_PTR for such cases.

Atribute possible_null

Attribute possible_null indicates that some function may return null value, which must be checked before dereferencing.

extern int*ppp;

__attribute__((svace_possible_null)) int* func() {
        return ppp;
}

void example1() {
        int* p = func();
        *p = 0;//svace: emitted DEREF_OF_NULL.RET.LIB
}

In the above code Svace will emit an warning DEREF_OF_NULL.RET.LIB, because pointer p is not checked for null.

Svace structure field’s attributes

Svace suppports attributes for fields of structures. During analysis Svace will treat those fields by special way, which depends on attribute semantic.

Attribute possible_negative

Attribute possible_negative marks structure fields, that they can have negative values.

struct struct1 {
    char* a;
    int b __attribute__((svace_possible_negative));
};

void test(struct struct1*p, int b){
    char buf[10];
    buf[p->b]=0;//NEGATIVE_CODE_ERROR
}

Attribute value_interval

struct struct1 {
    char* a;
    int b __attribute__((svace_value_interval(-3, -1)));
};

void example(struct struct1*p) {
    char buf[9]
    int v = p->b; //b can have only negative values    
    buf[v]; //NEGATIVE_CODE_ERROR
}

Atribute taint

Svace considers fields, which are marked by this attribute, as source of tainted string values.

struct struct1 {
    char* a __attribute__((svace_taint));
    int b;
};

char* extend(char* root, struct struct1*p) {
    char* str = p->a;
    
    //TAINTED_PTR was emitted, 
    //because length of `str` may exeed size of buffer, 
    //pointed by `root`.
    return strcat(root, str); 
}

Atribute taint_int

Svace considers fields, which are marked by this attribute, as source of tainted integer values. Those values should not be used in vulnerable operations without checking their ranges.

struct S {
        int a;
        int b __attribute__((svace_taint_int));
};

void example(struct S*s) {
        char buf[10];
        buf[s->b] = 0;//TAINTED_ARRAY_INDEX will be emitted
}

The attribute has another form with range. In this case Svace will assume that field can have any value in this range.

struct S {
        int a;
        int b __attribute__((svace_taint_int(10, 20)));
};

void error(struct S*s) {
        char buf[10];
        buf[s->b] = 0;//TAINTED_ARRAY_INDEX will be emitted
}

void no_error(struct S*s) {
        char buf[21];
        buf[s->b] = 0;//no error,because `s->b` has range [10;20].
}

Atribute possible_null

The attribute denotes, that field can have null value and its value must be checked before dereference.

struct struct1 {
    int* a __attribute__((svace_possible_null));
    int b;
};

int get_a(struct struct1*s) {
        int* p = s->a;
        return *p;//DEREF_OF_NULL.RET.LIB
}

Java annotations

Existing annotations

Language Java supports annotations for functions, function parameters and functions return values. Svace reacts on some popular annotations.

Not null annotations

Svace supports function parameters attributes NonNull and NotNull. Those attributes means that such functions should not get null value for this parameter.

public void someFunc(@NotNull String s) {
   //...
}

public void example(int i) {
  String s = i % 2 == 0 ? "even" : null;
  someFunc(s); //DEREF_OF_NULL.ANNOT.EX
}

Svace checks that function someFunc won’t get null value. For function example svace will emit a warning because string s can have null value.

In other tools they often are called models or annotations.↩︎
spec-functions↩︎

Introduction

Svace Description

Specifications Overview

Tutorial for C/C++

An Example Program

Using Specifications

Fixing The Error

Tutorial for Go

An Example Program

Using Specifications

Fixing The Error

C/C++ Specifications

Common Specifications

Execution Terminations

Overwrite Specifications

Working with Resources

Acquire and release specfunctions

Conditional acquire

Memory management specifications

Tainted Specifications

Sources of tainted values

Converting functions

Transferring taintedness

Sinks for tainted values

Sanitization

Buffers and Strings

Buffers

Nonterminated strings

Modeling strlen functions

Value properties

Negative values

Function results

Other Specifications

Initialization

Null pointer dereference

Lock-unlock

Other concurrency specifications

Variable argument functions

Vulnerable functions

sprintf, scanf-like functions

Sensitive data leaks

Exceptions

Combining Values

Specification for user checkers

Range checkers

Constant checkers

Guard checkers

Java/Kotlin specifications

Class hierarchy

Overridden methods

Context specification

Overview

Tutorial

An Example Program

Using Specifications

C/C++ Attributes

Regular attributes

Svace function attributes

Attribute value_interval

Attribute possible_negative

Atribute taint_int

Atribute taint

Atribute possible_null

Svace structure field’s attributes

Attribute possible_negative

Attribute value_interval

Atribute taint

Atribute taint_int

Atribute possible_null

Java annotations

Existing annotations

Not null annotations

Modeling `strlen` functions

`sprintf`, `scanf`-like functions