Skip to content

MARK Rules

Once the core functions of a library have been modeled as MARK entities, you can start writing rules. MARK rules operate over instances of entities and define conditions which must apply to these instances. A MARK "instance" may correspond to an actual object in the program, but in the case of non-object oriented languages or static methods, it may simply be an abstract set of function calls and variables.

Basic rule structure

MARK rules are structured as follows:

rule MyRule {
  using
    // instances go here
  ensure
    // conditions go here
  onfail
    // error message goes here
}

Each rule has a name which must be unique across along all MARK files loaded into Codyze. The using keyword starts the declaration of instances of MARK entities and the ensure keyword starts the actual condition. If Codyze finds a violation of the condition in the program, it will issue a finding with the message indicated by the onfail identifier.

To illustrate the process of writing MARK rules, let us assume we want to ensure that the MARK entity Crypto from the previous section uses either of the two cryptographic algorithms Algo1 or Algo2 and that the algorithm is initiated with a parameter which is longer than 16 bytes.

rule ID_2 {
  using
    Crypto as c,                   // instance c of MARK entity Crypto
    CryptoParameter as cp          // instance cp of MARK entity CryptoParameter
  ensure
    _is(c.param, cp)               // variable c.param == cp
    && _length(cp.rawData) >= 16   // byte length of cp.rawData >= 16
  onfail
  // todo
}

Preconditions

Some rules only apply if certain preconditions are fulfilled, i.e. such preconditions will be evaluated before the actual condition. If they fail, the main condition will not be evaluated and the rule will not return any result (i.e. it will neither confirm a valid program nor flag a wrong program). Preconditions follow the same syntax as the main condition, but are declared by the when keyword.

rule ID_2 {
  using
    Crypto as c,                   // instance c of MARK entity Crypto
    CryptoParameter as cp          // instance cp of MARK entity CryptoParameter
  when
    c.algorithm == "Algo1"         // rule is only relevant for "Algo1"
  ensure
    _is(c.param, cp)               // variable c.param == cp
    && _length(cp.rawData) >= 16   // byte length of cp.rawData >= 16
  onfail
  // todo
}

Built-in Predicates

MARK comes with a number of built in functions that can be used as predicates in conditions and preconditions. These built-ins are called when MARK rules are evaluated and operate over their input arguments (typically MARK objects or constants) and the current evaluation context. By convention, built-ins should start with an underscore (_). When a built-in fails, it will return an Error object that always evaluates to not applicable, i.e. neither true nor false.

_between

Function: _between(String str, String start, String end)

Example:

  ensure
     _between("<09>", "<", ">") == "09"
Returns the part of the string between start and end which both have to be part of the string. If start or end are not part of the string, this returns an Error.

_direct_eog_connection

Function: _direct_eog_connection(Node n1, Node n2)

Example:

  ensure
     _direct_eog_connection(n1, n2)
Checks if there is a direct EOG-connection (i.e., without branches) between the two given vertices.

_eog_connection

Function: _eog_connection(Node n1, Node n2)

Example:

  ensure
     _eog_connection(n1, n2)
Checks if there is an arbitrary EOG-connection between the two given vertices.

_get_code

Function: _get_code(a)

Example: TODO

Returns the corresponding source code of MARK object a. If this is not possible, this returns an Error.

_has_value

Function: __has_value(a,b)

Example:

  ensure
     __has_value(a, b)
Returns true if MARK object a may be assigned value b (e.g., a constant).

_inside_same_function

Function: __inside_same_function(a,b)

Example:

  ensure
     __inside_same_function(a, b)
Returns true if MARK objects a and b reside in the same function.

_is

Function: _is(a,b)

Example:

  ensure
     _is(a, b)
Returns true if MARK object a is equal to variable b.

_is_instance

Function: _is_instance(a, String classname)

Example:

  ensure
     _is_instance(a, "java.lang.String")
Returns true if MARK object a is an instance of classname. classname has to be the fully qualified name of the class.

_length

Function: _length(a)

Example:

  ensure
    _length(a) == 5 // e.g. for array declaration `new int[5]`
Returns the length of MARK object a. Currently, this can only return the dimension of an Java array.

_now

Function: _now()

Example:

  ensure
    _now() == 1653955200 // 2022-05-31T00:00:00Z
Returns the current time as the number of seconds since epoch (1970-01-01T00:00:00Z). Relies on Java's Instant.now().

_receives_value_from

Function: _receives_value_from(a,b)

Example:

  ensure
     _receives_value_from(a, b)
Returns true, if there is a data flow from a to b.

_split

Function: _split(String str, String splitter, int position)

Example:

  ensure
     _split("ASD/EFG/JKL", "/", 1) == "EFG"
Behaves like the Java expression String.split(String splitter)[position]. That is, it splits the string str at all occurrences of splitter and returns the positionth substring. Returns an Error if no such occurrence is found.

_split_disjoint

Function: _split_disjoint(String str, String splitter, List set)

Example:

  ensure
     _split_disjoint("ASD/EFG/JKL", "/", ["ABC", "EFG", "JKL"])
Splits str at all occurrences of splitter and checks, if any of the resulting elements is part of the provided set. Returns an Error if no occurrence of split is found.

_split_match_unordered

Function: _split_match_unordered(String str, String splitter, List set, Boolean strict)

Example:

  ensure
     _split_match_unordered("ASD/EFG/JKL", "/", ["ASD", "EFG", "JKL"], true)
Splits str at all occurrences of splitter and checks, if resulting elements are part of the provided set. The optional parameter strict controls if the set resulting from splitting should be identical to the provided set. Returns an Error if no occurrence of split is found.

_starts_with

Function: _starts_with(String str, String start)

Example:

  ensure
     _starts_with("ASDEFGJKL", "ASD")
Returns true if str starts with start.

_year

Function: _year(Int time)

Example:

  ensure
    _year(1653955200) == 2022 // 2022-05-31T00:00:00Z
Returns the year in which time is in. time represents the number of seconds since epoch (1970-01-01T00:00:00Z).


Last update: 2022-08-23
Created: 2020-01-16