# Divide By Zero (`zk-divide-by-zero`

)

## Summary and Usage

The Divide By Zero (DBZ) detector is used to identify potential divide-by-zero errors in ZK circuits. Divide-by-zero errors can lead to significant security risks, as malicious actors may be able to create valid proofs for bogus statements.

### Usage

The DBZ detector is invoked by selecting "Divide by zero (ZK)"
(`zk-divide-by-zero`

) in the Detector selection during the tool configuration step.

## Example and Explanation

In the following example, the `Divide`

circuit has been developed to compute the
`quotient`

of `dividend`

divided by `divisor`

.
In finite prime field arithmetic, as is performed in circom (i.e., all operations performed modulo the prime $p$),
division is implemented as multiplication by the inverse of the divisor,
Formally, this computation is:

`pragma circom 2.1.8;`

template Divide() {

signal input dividend;

signal input divisor;

signal output quotient;

quotient <-- dividend / divisor;

quotient * divisor === dividend;

}

component main = Divide();

The intended behavior of this circuit is for `out`

to be set to `in1 / in2`

.
This performed by first assigning `out <-- in1 / in2`

, then generating the constraint
of `out * in2 === in1`

(which is done because constraints cannot contain division operations,
as they result in non-quadratic constraints).
However, this constraint does not enforce the requirement that `in2`

cannot be
0 in order for `in1 / in2`

to be a valid operation; in other words, the developer
did not intend for 0 to be a valid assignment for `in2`

.
Therefore, the constraints of the circuit can be satisfied by the
following assignment: `in1 = 0, in2 = 0, out = 5`

, as this satisfies the circuit's
constraint (`5 * 0 === 0`

).
However, this clearly deviates from the developer’s intention,
which was for `out`

to be set to `in1 / in2`

and for `in2`

to be non-zero.

## Usage Example

Running the DBZ detector yields the following text output log:

## ZK Vanguard Output

`----Running Vanguard with zk-divide-by-zero detector----`

Running detector: zk-divide-by-zero

[Critical] Found signal in component that are used as divisors and could cause a division by zero Divide @ divide_bug.circom:3

Reported By: vanguard:zk-divide-by-zero

Location: Divide @ divide_bug.circom:3

Confidence: 0.99

More Info: placeholder

Details:

Found signal in component that are used as divisors and could cause a division by zero Divide @ divide_bug.circom:3

* Signal divisor in expression Divide @ divide_bug.circom:7

Line 3 of the above log tells us that there is a division operation that uses a signal as a
divisor in the `Divide`

component (defined on line 3 in `divode_bug.circom`

).
Lines 9–10 of the log then tell us that signal is `divisor`

and that the possible divide-by-zero error
occurs on line 7 in `divide_bug.circom`

.

## Limitations

This detector does not evaluate the possible values of expressions used in divisors, instead flagging all division operations as possible divide-by-zero concerns. This means that divisor expressions that are explicitly constrained to be non-zero will incur false positives.

## Assessing Severity

If it is manually determined that the divisor of a division operation may be zero, the circuit may contain a critical vulnerability, as unexpected signal values may be used to generate a valid proof.