Function contracts and roles¶

Visao knows what a library function does from its contract. A contract is an ACSL block that is attached to a function by its symbol name. The analyzer does not know any function by its name. It reads the contract and the roles in the contract.

Contract files¶

Contract files have the .contract extension. The format is:

# comment
@symbol read(fd, buf, count)
/*@
  @ requires count == 0 || \valid(buf + (0 .. count - 1));
  @ tagged "role:input", "role:writes:1";
  */

The @symbol line gives the symbol and the names of its parameters. Visao binds the names to the parameters of the real declaration by position, so the host header can use other names.

Visao reads contracts from these directories:

<stdlib>/c/contracts/: Contracts of C and C++ library functions: the C standard library, POSIX, Linux, macOS and Windows. C, C++, Objective-C, RuC and assembly use these contracts.
<stdlib>/LANGUAGE/contracts/: Contracts of the library functions of one language, for example <stdlib>/python/contracts/ or <stdlib>/java/contracts/. The directory name is the language name of the --language option.
<stdlib>/roles/: Roles of names that the frontends make for every language, for example !throw. Visao reads only the roles from these files.

A contract applies only to the analysis of its language. The Python open and the C open are two different functions with two different contracts.

Visao finds the contract of a call by the name of the called function:

When the program or a library model declares the function, Visao attaches the contract to the declaration.
When the program calls a function that it does not declare, Visao attaches the contract to the called function at the first call.

The name and the arguments of a call are the ones the frontend gives the call:

A method call x.m(a) calls m with the arguments x, a. The receiver is argument 0, so the contract is @symbol m(self, a).
A call through an imported module keeps the module name: the Python os.system(c) calls os.system with the argument c.
A Rust path keeps the last part: File::open(p) calls open.

Rules for the ACSL block of an entry:

Write the requires clauses before the ensures clauses. The ACSL grammar sets this order.
Do not give a parameter the name of an ACSL keyword, for example default.
Use p != \null for “not null”. In a script language, write it only for an argument that is never a number: the value \null is 0.

An entry with only tagged clauses gives roles. Visao does not attach it, and the call stays unknown to the value analysis.

One symbol can have entries in more than one file. Visao adds the roles of all entries together. An entry that has ACSL clauses other than tagged replaces the ACSL block of an earlier entry.

A function in the analyzed source can have roles too. Write the roles in the annotation of the function:

/*@ tagged "role:input"; */
int read_packet(char *buf, int len);

System state¶

A contract can read and change the state of the system the program runs on: the operating system, the CPU, the hardware and the threads. The state is a set of state variables. A state variable is a number that exists only in the analysis.

Declare a state variable in a contract file:

@state os_irq_off = 0
@balanced os_irq_off
@state os_context = 0
@entry hardirq os_context = 2, os_irq_off = 1

@state NAME = VALUE: Declares the state variable NAME. Each function starts with the variable at VALUE.
@balanced NAME: Each function must return with NAME at the value it had when the function started. Visao checks this at each return and at the end of the function.
@entry PROFILE NAME = VALUE, ...: Gives the values a function starts with when the system runs it in the way PROFILE names, for example as an interrupt handler.

A contract uses a state variable by its name. In an ensures clause, \old(NAME) is the value before the call:

@symbol local_irq_disable()
/*@ ensures os_irq_off == \old(os_irq_off) + 1; */

@symbol msleep(ms)
/*@ requires \report(os_irq_off == 0 && os_context == 0,
                     "WrongExecutionContext"); */

These roles give a function its entry profile:

role:handler:N:PROFILE: The function passed in argument N runs with the entry profile PROFILE. Use it on the function that registers a handler, for example request_irq or signal.
role:entry:PROFILE: The function runs with the entry profile PROFILE. Write it on an interrupt handler in the analyzed source.

A function called in a function of the program shares the state of its caller. The program can call a function it defines. Then Visao checks the state requirements of the library calls that this function makes before its first branch or return.

The findings of this section:

WrongExecutionContext: A call needs another state of the system.
StateNotRestored: A function returns with a balanced state variable at a value other than the one it started with.

The models of the target systems are in these directories. They apply to the C family:

<stdlib>/os/OS/contracts/: The model of the target OS: linux, macos, windows or baremetal. <stdlib>/os/posix/contracts/ applies to Linux and macOS.
<stdlib>/cpu/CPU/contracts/: The model of the target CPU, for example arm or x86_64.

An entry of a system model adds its clauses to the library contract of the same symbol. The target comes from the build. The environment variables VISAO_MODEL_OS and VISAO_MODEL_CPU select another model, for example to analyze kernel code with the headers of the host.

Function summaries¶

Visao analyzes each function of the program on its own. A call of a function of the program uses the contract of that function. A function without a contract gets a summary from the analysis of its body:

the range of its result, for example \result >= 1 && \result <= 3;
a result that is never null;
the change the function makes to a state variable, for example os_irq_off == \old(os_irq_off) + 1.

Visao analyzes the called functions before their callers, so the caller gets the summary. A function with no branch and no early return that changes a balanced state variable is a wrapper, for example a lock function. Visao does not report StateNotRestored for it. Its callers get the change through the summary.

The caller uses the range of a result in the same way as the range of a variable. This is also true for a call in a condition, for example if (pick(a) > 10). When the range of each operand makes the condition always true or always false, Visao reports ConditionAlwaysTrue or ConditionAlwaysFalse. An outer condition also gives a range, for example x < 1 is always false in the body of if (x >= 1). Visao uses the relations between variables too: in the body of if (x < y && y < 10) the condition x > 20 is always false. A loop stops when its condition is false or at a break. After the loop, a variable has one of the values it has at these points. After for (i = 0; i < 10; i++) the condition i < 5 is always false. After while (i < 100) { if (c) break; i++; } the condition i > 100 is always false. A continue gives its values to the next iteration. In the body of a loop the ranges hold for all iterations: in the same loop i > 20 is always false, and i == 5 gives no finding.

Calls between languages¶

A function of the program with a contract or a summary is available to the other languages of the run under its name. A call from another language uses that contract: Visao checks the requires clauses at the call and uses the ensures clauses after it.

These calls get the contract:

a call through Python ctypes or cffi, for example lib.foo(x);
a function in a Rust extern "C" block;
a Go call through cgo, for example C.foo(x);
a C# method with DllImport;
a Java native method. The C function Java_pkg_Class_method gives its contract to the method method, without the two JNI parameters.

When the analysis of the function finds a violated ensures clause, the contract is refuted. The callers then check its requires clauses and do not use its ensures clauses.

Visao analyzes C, C++, Rust and Go files before the other languages of the run, also with -j. The functions these languages export are then known when a Python, Java or C# file calls them.

Roles¶

A role is a string in a tagged clause. It starts with role:. Some roles have parameters. A parameter is separated by :. Argument numbers start at 0. In a method call, argument 0 is the receiver.

Resources¶

role:acquire:CLASS

The result is a new resource of the class CLASS.

role:acquire_on_success:CLASS

The result is a new resource of the class CLASS only when the call succeeds.

role:release:CLASS:N

The function releases the resource in argument N. The class tells what the release does:

memory, malloc, new, new[] and gc free memory.
mutex, rwlock, spin and lock unlock.
The other classes close a handle.

role:lock:CLASS:N

The function locks the lock in argument N.

role:alloc_size:N

The size of the new block is argument N. role:alloc_size:N*M gives the size as the product of two arguments.

role:reallocates:N

The function releases the block in argument N and returns a new block (realloc). The facts about the old block become false.

role:nullable_result

The result can be null. A use of the result before a check is a defect.

The rules use these resource classes:

Memory: malloc, malloc0 (zeroed memory), new, new[], gc, stack, heapmem (HeapAlloc), local, global, cotask, bstr, aligned, malloca, vm, and the reference-counted cf, objc and dispatch. A release frees the memory.
Locks: mutex, rwlock, spin, lock, srw. A release unlocks.
Handles: every other class, for example FILE, fd, DIR, pipe, db, handle (a Windows handle), heap (a heap from HeapCreate), find, module (a loaded library), map (a mapped view), key (a registry key). A release closes the handle. A handle that is not closed is a handle leak.

The class sets are in XResourceTracker::isMemoryClass, isLockClass and isHandleClass.

Control flow¶

role:abort: The function does not return.
role:assert: The function is an assertion handler. It stops the program because an assertion failed.
role:branch_hint: The function returns its argument 0 and tells the compiler which branch is likely (__builtin_expect).

Data from outside¶

role:input: The function reads data from outside the program. Its result and the buffers it writes are tainted.
role:input:function: The same, but only when the call is a function call, not a method call (Go fmt.Scan against rows.Scan).
role:taint_passes: The result is tainted when an argument is tainted (atoi).
role:sink:KIND: The function interprets its argument. KIND is command (runs a program), command_shell (only with shell=True) or code (evaluates code). A tainted argument is an injection.
role:secret_source: The result is a secret (a password hash, a key).
role:secret_passes: The result is a secret when an argument is a secret.
role:copies:D:S: The function copies argument S into argument D.

Buffers and memory¶

role:writes:N: The function writes into the buffer in argument N.
role:bounded_copy:N: The function copies a bounded string into argument N and can leave it without a terminating null (strncpy).
role:mem_copy:D:S:L: The function copies L bytes from argument S to argument D. The regions must not overlap.
role:mem_move:D:S:L: The same, but the regions can overlap (memmove).
role:mem_fill:D:L: The function writes L bytes into argument D.
role:derefs:N: The function reads through the pointer in argument N. A null pointer there is a defect.
role:borrows:N: The function uses the block in argument N only while it runs. It does not free the block or keep a pointer to it, so the caller still owns the block (strcpy, memcpy).
role:size_arg:N: Argument N is a size.
role:var_param:N: Argument N is a Pascal var or out parameter. The call passes the variable, and the function can write into it (TryStrToInt).
role:returns_into:N: The result points into the buffer in argument N.
role:format:N: The format string of a printf-like function is argument N.
role:format_scan:N: The format string of a scanf-like function is argument N.
role:unbounded_format_write:N: The function writes formatted text into argument N without a size (sprintf).

Paths¶

role:path_check:N: The function checks the file in argument N (access, stat).
role:path_use:N: The function acts on the file in argument N (open, unlink). A check before a use of the same path is a race.

Security¶

role:compares:A:B: The function compares argument A with argument B.
role:variable_time_compare: The comparison stops at the first difference. It leaks the position of that difference through time.
role:credentials:L:P: The function takes a login in argument L and a password in argument P. Use -1 when the function has no login argument.
role:security:KIND: The function is part of the security surface. KIND is password, authorization, authentication, crypto, token or privilege.
role:dangerous: The function cannot be used safely (gets, tmpnam).
role:banned:STANDARD:RULE: A coding standard bans the function, for example role:banned:misra-c-2012:21.6.

Findings on a call¶

The frontend rules of a language use these roles. A rule reports only the finding types that it owns, so the same name in two languages does not mix the rules.

role:report_call:TYPE: A call of the function is a finding of the type TYPE. TYPE is a report type name, for example EvalCall.
role:report_string_arg:TYPE:N: A call with a string literal in argument N is a finding of the type TYPE. The function runs that string as code (setTimeout("code", n)).
role:returns_minus_one_if_missing: The function returns -1 when it does not find the value (indexOf).
role:deletes_files: The command deletes files (rm).
role:blocking_wait: The method blocks the thread until the task in the receiver completes (C# Task.Wait).
role:builtin: The name is a builtin of the language. An assignment to the name hides the builtin (Python list = []).
role:existence_check: The function tests whether a value exists. It does not use the value (PHP isset).
role:glob_mode:N: Argument N selects the mode of the command. The modes GLOB and GLOB_RECURSE find the files one time, at configure time (CMake file).
role:minimum_version: The command sets the minimum version of the tool and the policies of that version (CMake cmake_minimum_required).

Signals¶

role:async_signal_safe: The function can be called from a signal handler.
role:signal_handler:N: The function installs the signal handler in argument N.

Containers¶

role:container:OP and role:container:OP:N: A container operation. OP is create, sized (the size is argument N), empty, grow, shrink, clear, len or read.
role:iterator: The result is an iterator into the receiver.
role:invalidates_iterators: The function changes the storage of the receiver. Iterators into the receiver become invalid.
role:indexed:N: Argument N is an index into the receiver.
role:consumes_receiver: The function moves the receiver. A later use of the receiver is a defect.

Values¶

role:math:FUNCTION: The function computes a known mathematical function, so the analyzer can compute the result of a call with known arguments. FUNCTION is abs, fabs or sqrt. abs computes the absolute value of an integer argument. fabs also computes it for a floating argument.