Main Content

-create-checkers

Create new checkers for Polyspace Bug Finder analysis

Since R2023b

Syntax

-create-checkers file1[,file2[,...]]

Description

-create-checkers file1[,file2[,...]] specifies Datalog files (.dl files) that define new checkers for a Polyspace® Bug Finder™ analysis. The checker definitions use a Datalog-based API for specifying code elements and behaviors that together make up the checker. To define a checker using this option:

  1. Reformulate the checker definition into a form that allows data flow analysis between code elements (functions, variables, etc.) with specific behaviors.

    In other words, fill up the missing spaces in the following line: There should not be a data flow from element ___ with behavior __ to element ___.with behavior ___.

  2. Write down the code elements and behaviors using the Datalog-based API into a checker definition file.

For information on supported behaviors, see Modify Bug Finder Checkers Through Code Behavior Specifications.

This option is similar to the option -code-behavior-specifications with some key differences.

-code-behavior-specifications-create-checkers

This option modifies the default specifications of existing checkers.

This option creates new checkers.

The Datalog file specifying the checker modifications lists the code behaviors that modify the checker.

For instance, to modify the default specifications of an SQL injection checker, you might specify behaviors in the following format:

.include "models/interfaces/sql.dl"

Sql.Basic.execution("sql_exec", $InParameterDeref(0)).
Sql.Basic.sanitizing("sql_sanitize", $OutParameterDeref(0)).
This file specifies that the checker, in addition to the predefined behaviors, must also incorporate the following behaviors:

  • The dereference of the first parameter of the function sql_exec() must be considered as sensitive to SQL injection.

  • The dereference of the first parameter of the function sql_sanitize() must be considered as sanitized after the function call.

The Datalog file specifying the checker definition lists the code behaviors defining the checker inside a checker configuration and then initializes the checker with the configuration.

For instance, to create the checker Tainted source used with sensitive function, you might specify behaviors in the following format:

.include "models/interfaces/tainted_source_use_custom.dl"
.include "pql/checkers/tainted_source_use_custom_impl.dl"

.comp checkerConfig : CustomTainted {
    Basic.taintSource("getResponse",$OutReturnValue(),"Data from getResponse() is tainted.").
    Basic.sensitive("changeSystemState",$InParameterValue(0),"changeSystemState() must not use tainted data.").
    Basic.sanitizing("ensureSafeResponse",$OutParameterDeref(0)).
}

.init customTaintedChecker = tainted_source_use_custom<checkerConfig>

This file specifies that the checker is defined using the following behaviors:

  • The dereference of the return value of the function getResponse() must be considered as a taint source.

  • The dereference of the first parameter of the function changeSystemState() must be considered as a function vulnerable to a tainted source.

  • The dereference of the first parameter of the function ensureSafeResponse() must be considered as sanitized after the function call.

This option when used modifies the behavior of all checkers associated with the option.

This option allows you to create separate instances of a checker with separate behaviors.

For instance, you can define multiple checker configurations as follows:

.include "models/interfaces/tainted_source_use_custom.dl"
.include "pql/checkers/tainted_source_use_custom_impl.dl"

.comp checkerConfig1 : CustomTainted {
    Basic.taintSource("getResponse1",$OutReturnValue(),
    "Data from getResponse() is tainted.").
    Basic.sensitive("changeSystemState1",$InParameterValue(0),"changeSystemState() must not use tainted data.").
}

.comp checkerConfig2 : CustomTainted {
    Basic.taintSource("getResponse2",$OutReturnValue(),"Data from getResponse() is tainted.").
    Basic.sensitive("changeSystemState2",$InParameterValue(0),"changeSystemState() must not use tainted data.").
}

.init customTaintedChecker1 = tainted_source_use_custom<checkerConfig1>
.init customTaintedChecker2 = tainted_source_use_custom<checkerConfig2>
The two configurations checkerConfig1 and checkerConfig2 define two separate instances of a checker (even though both checkers are named Tainted source used with sensitive function):

  • The checker with configuration checkerConfig1 flags flow of unsanitized data from getResponse1() to changeSystemState1().

  • The checker with configuration checkerConfig2 flags flow of unsanitized data from getResponse2() to changeSystemState2().

You do not see a cross-connection between the two checkers. For instance, there is no defect for flow of unsanitized data from getResponse() to changeSystemState2().

This option supports behavior specification in XML and Datalog format.

This option supports behavior specification in Datalog format only.

The Datalog file specifying behaviors only needs to include behavior declarations from the subfolder models/interfaces.

For instance, to modify the default specifications of an SQL injection checker, you might specify behaviors in the following format:

.include "models/interfaces/sql.dl"

Sql.Basic.execution("sql_exec", $InParameterDeref(0)).
Sql.Basic.sanitizing("sql_sanitize", $OutParameterDeref(0)).
This file includes the Datalog file models/interfaces/sql.dl, which contains declarations of the behaviors, Sql.Basic.execution and Sql.Basic.sanitizing.

The Datalog file specifying behaviors needs to include:

  • Behavior declarations from the subfolder models/interfaces.

  • Checker implementations from the subfolder pql/checkers.

For instance, to create the checker Tainted source used with sensitive function, you might specify behaviors in the following format:

.include "models/interfaces/tainted_source_use_custom.dl"
.include "pql/checkers/tainted_source_use_custom_impl.dl"

.comp checkerConfig : CustomTainted {
    Basic.taintSource("getResponse",$OutReturnValue(),"Data from getResponse() is tainted.").
    Basic.sensitive("changeSystemState",$InParameterValue(0),"changeSystemState() must not use tainted data.").
    Basic.sanitizing("ensureSafeResponse",$OutParameterDeref(0)).
}

.init customTaintedChecker = tainted_source_use_custom<checkerConfig>
This file includes the Datalog file models/interfaces/tainted_source_use_custom.dl with the behavior declarations as well as the Datalog file pql/checkers/tainted_source_use_custom_impl.dl with the checker implementations.

Examples

Suppose you want to create the checker Tainted source used with sensitive function by specifying the following information:

  • The return value of the function getResponse() is untrusted.

  • The function changeSystemState() is a sensitive function that is vulnerable to attacks via its first argument and must not use untrusted data.

To create this checker:

  • Specify the required information in a checker definition file (for instance, customTaintChecker.dl) written as follows:

    .include "models/interfaces/tainted_source_use_custom.dl"
.include "pql/checkers/tainted_source_use_custom_impl.dl"

.comp checkerConfig : CustomTainted {
    Basic.taintSource("getResponse",$OutReturnValue(),"Data from getResponse() is tainted.").
    Basic.sensitive("changeSystemState",$InParameterValue(0),"changeSystemState() must not use tainted data.").
}

.init customTaintedChecker = tainted_source_use_custom<checkerConfig>

  • Specify this checker file as argument to the option -create-checkers and also enable the checker Tainted source used with sensitive function:

    polyspace-bug-finder -create-checkers customTaintChecker.dl -checkers TAINTED_SOURCE_USE_CUSTOM
    Or:
    polyspace-bug-finder-server -create-checkers customTaintChecker.dl -checkers TAINTED_SOURCE_USE_CUSTOM

The newly created checker flags cases where there is a data flow from the return value of the getResponse() function to the first argument of the changeSystemState() function.

The simplest example of such a data flow looks like this:

extern int getResponse(void);
extern void changeSystemState(int); 

void main() {
    int response = getResponse();
    changeSystemState(response);
}

Version History

Introduced in R2023b

See Also

Topics