We provide an algebraic approach in hardware verification for checking of properties of hardware systems, finding vulnerabilities and model-based testing. We developed a line of tools for these purposes. The technology consists of the number of stages operating with formal specifications.
1. Formalization of hardware specifications.
We convert VHDL or System Verilog specifications into the algebraic specifications of behavior algebra.
Here the example of the translation of the FPGA algorithm.
The behavior specifications:
B0 = P1 || P2 || P3,
P1 = (Aor2(or2_1, ENV, ENV, and) || Aor2(or2_2, ENV, ENV, and)) ; Aand (and, or2_1, or2_2, ENV),
P2 = Atctc_filtered(tctc_filter, ENV, ENV, 3000) +
Atctc_not_filtered(tctc_filter, ENV, ENV, 3000),
P3 = Amul_fp(mul_fp, ENV, ENV, cmpc_fp_gr, switch_fp, or4, or4, or4);
Acmpc_fp_gr (cmpc_fp_gr, mul_fp, switch_fp, or4, 5000, 0);
(Aor4(or4, cmpc_fp_gr, mul_fp, mul_fp, mul_fp, ENV) ||
Aswitch_fp(switch_fp, cmpc_fp_gr, mul_fp, ENV, ENV))
Actions specifications:
|
Actions with parameters |
Precondition |
Process component |
Postcondition |
|
Acmpc_fp_gr(s, x1, x2, y, setpoint:real, hysteresis:real) Local parameters: (in:real, out:bool, nan:bool) |
1
|
receive(x1 : signal(in)), send(x2 : signal (out), signal (y : nan)) |
out = (in > setpoint – hysteresis) |
|
Aor2(s, x1, x2, x3) Local parameters: (in_1, in_2, out : bool) |
1 |
receive(x1: signal (in_1)), receive(x2: signal (in_2)), send(y : signal(out)) |
out = (in_1 || in_2) |
|
Aor4(s, x1, x2, x3, x4, out) Local parameters: (in_1, in_2, in_3, in_4, out : bool) |
1 |
receive(x1: signal (in_1)), receive(x2: signal (in_2)), receive(x3: signal (in_3)), receive(x4: signal (in_4)), send(y: signal(out)) |
out = (in_1 || in_2 || in_3 || in_4) |
|
Aand(s, x1, x2, y) Local parameters: (in_1,in_2,out : bool) |
1 |
receive(x1: signal (in_1)), receive(x2: signal (in_2)), send(y: signal(out)) |
out = (in_1 && in_2) |
|
Amul_fp(s, x1, x2, y0, y1, y2, y3, y4) (in_1:real, in_2:real, out:real, overflow:bool, underflow:bool, nan:bool) |
1 |
receive(x1 : signal(in_1)), receive(x2 : signal(in2)), send(y0:signal(out)), send(y1:signal(out)), send(y2:signal(overflow)), send(y3:signal(underflow)), send(y4:signal(nan)) |
out = (in_1 * in_2); overflow = (out >maxReal32); underflow = (out <minReal32) |
|
Atctc_filtered(s, x, y, n) |
(TIMER == 0) |
receive(x : signal (in)), send(y : signal (out)) |
in == out |
|
Atctc_filtered(s, x, y, n) |
(TIMER == 1) |
receive(x : signal (in)) |
1 |
|
Aswitch_fp(s, x1, x2, x3, y) Local parameters: (sel:bool, in_x1:real, in_x2:real, out:real) |
1 |
receive(x1 : signal(in_x1)), receive(x2 : signal(in_x2)), receive(x3 : signal(sel)), send(y:signal(out)) |
(sel == 0) && (out == in_x1) || (sel == 1) && (out == in_x2) |
2. Verification stage.
Model verification is to investigate the behavioral properties of safety or viability.
Formal methods of behavior algebra that are used to prove the reachability of the properties, that being tested, can be static, dynamic, combined, and partially dynamic. The input into the verification procedure is a model in the form of behavior algebra and a formula of the property that is tested and the output is a verdict that confirms its reachability and scenario that leading to the corresponding state.
Static methods are the methods, for which it is sufficient to prove the property of feasibility that is given by the formula in the base language, i.e., there are such values of formula attributes with which the formula can be true. Proof of the property of feasibility is achieved by the use of solver machines such as Microsoft Z3 and cvc4.
Dynamic methods are applied to behavioral properties, i.e., the properties where a formula is represented by expressions of behavior algebra and by semantic of actions, where a formula is represented as an expression in the base language. Such methods use the methods of symbolic modeling and methods of solving the system of behavioral equations. All these methods of behavior algebra are presented in paper 1 and paper 2(pp. 118-130).
Combined methods are those for which proving the feasibility of formulas is not sufficient, and it is necessary to prove the formula's reachability by symbolic modeling. Partially dynamic methods use the technique of invariants generating in behavior algebra.
The main verification methods that are applied to hardware within the behavioral algebra are:
- incompatibility (nondeterminism) in algorithms of schemes is checked by the statically feasibilities of the formula /\ia(i)=0, where а(і) is a prerequisite of action;
- incompleteness (deadlocks) in the algorithms of schemas is checked by the formula's feasibility \/ia(i)=0;
- compatibility of time properties and synchronization problems. These properties are verified by the symbolic modeling of behavioral equations from some initial state that is given by the formula above the attribute environment. In modeling, the pre-condition and the current state of the environment, are checked for feasibility and, if it's present, the state of environment changes according to the post-condition;
- critical states (are defined by the formula above the attribute environment), which express a state of "starvation", when all agents are waiting to receive signals, a state of violation, or other security properties that can be specified by the user. Such properties can be both local (annotations in the design code, assertion) and global;
- signal race, when different signal acquisition sequences create different states of the environment, - are checked by symbolic modeling or invariant generation;
- life properties, expressing the attainability of the desired state, is checked by symbolic modeling.
3. Model-based testing.
The algebraic model can be used as a model for the generation of trails that are used to create a test set in a suitable testing environment. Verification of compliance model artifacts can occur at each phase of development. Both design specifications and binary code can be tested. The main methods of test generation are direct and inverse symbolic modeling. The requirements for test generation determine the required coverage of code lines by tests.
Coverage is also determined by a model where comprehensive testing can be considered, i.e. generating of all possible states of model behaviors, covering of actions in the model, or covering of all transitions between actions. In hardware, the sequence of receiving and sending of signals between agents is considered as a test. When performing tests, distinguished the instance that tests and the instance that being tested. In this process, the signals are sent to the test instance and compared with the expected result.
The following types of testing are considered when using behavior algebra:
- black-box testing with a set of tests where the code of the instance being tested is unknown;
- white box testing, where the process is determined by the symbolic execution of the parallel model and code composition. When performed, states of the environment are compared for equivalence.
4. Vulnerabilities detection.
Behavioral Algebra models give us a possibility to evaluate the algorithm's ability to withstand attacks by intruders and, accordingly, to detect the vulnerable behaviors in the models. Such vulnerabilities include data leakage or the ability to overwrite the information in FPGA. When evaluating resilience to attacks that lead to errors, the system's ability to store sensitive information is analyzed.
Vulnerable or attacker behavior is modeled by using templates. A template is an expression in a behavior algebra that contains actions that present vulnerabilities and unknown behaviors that lead to them. For example, if we have actions of reading information A and receiving a signal containing the read information, then the pattern has the form of the following behavior:
S = read(A).X;send(A)
where X is an arbitrary behavior.
The task is to find the behavior of the X in the model and those that lead to these actions. This problem is solved in two stages.