Fuzzing report: 13 bugs found in CUDD 4.0.0-rc2 via Hopper

[HudsonCollier]

Summary

We fuzzed CUDD 4.0.0-rc2 using Hopper (an API-aware fuzzer) as part of a university course project. Hopper generated 173 crashes which we de-duplicated and then investigated the 13 strongest candidates. We wrote standalone C reproducer programs for each one and cross referenced them against the official CUDD API documentation.

2 of the 13 bugs violated the API documentation, shown below with reproducers and ASAN output. 11 of the 13 bugs involve API misuse meaning that the library crashes rather than returning an error, but the user violated the documented API contract. We include them at the bottom of the report for completeness.

All reproducer files, triage scripts, and ASAN output are available at:
https://github.com/Boolean-Fuzzers/CUDD-Fuzzing (hopper branch, triage/ directory)

Bug 1: Cudd_FactoredFormString crashes when inames is NULL

Crash ID: id_000007

Reproducer

#include "cudd.h"

int main() {
    DdManager *dd = Cudd_Init(1322, 113, 263, 5, 220);
    DdNode *f = Cudd_ReadMinusInfinity(dd);
    char *result = Cudd_FactoredFormString(dd, f, NULL); 
    Cudd_Quit(dd);
    return 0;
}

ASAN Output

AddressSanitizer: SEGV on unknown address 0x000000000000
#0 in Cudd_bddIsVar (libcudd.so)
#1 in ddDoFactoredFormString (libcudd.so)
#2 in Cudd_FactoredFormString (libcudd.so)

Bug 2: Cudd_AddHook silently stores NULL, causing crash in Cudd_ReduceHeap

Crash ID: id_000152

Reproducer

#include "cudd.h"

int main() {
    DdManager *dd = Cudd_Init(679, 979, 6, 206, 43);
    Cudd_AddHook(dd, NULL, CUDD_PRE_REORDERING_HOOK);  
    Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT, 46); 
    Cudd_Quit(dd);
    return 0;
}

ASAN Output

AddressSanitizer: SEGV on unknown address 0x000000000000
pc points to the zero page (null function pointer called)

API Misuse Candidates

The following crashes involve inputs that deviate from the documented CUDD API contract. We document them in case the maintainers wish to add defensive error handling, and flag three items that may warrant closer inspection despite being triggered by misuse.

#	Function	Crash Type	Crash ID	Notes
1	Cudd_NextCube	Stack overflow	id_000004	Generator from Cudd_FirstPrime passed to Cudd_NextCube, which is documented to work only with Cudd_FirstCube generators
2	Cudd_NextPrime	Null ptr deref	id_000001	NULL passed as cube output pointer
3	Cudd_BddToCubeArray	Stack overflow	id_000033	Array smaller than Cudd_ReadSize(dd): docs require one entry per BDD variable
4	Cudd_FirstPrime	Internal crash	id_000003	ZDD node passed where BDD node required. The manual states types must not be mixed
5	Cudd_bddVectorCompose	Null ptr deref	id_000080	NULL passed for the vector parameter
6	Cudd_SubsetWithMaskVars	Illegal free()	id_000124	See note below
7	Cudd_IterDerefBdd	Cross-manager	id_000136	Node from manager A passed to manager B
8	Cudd_EquivDC	Null ptr deref	id_000011	NULL passed for required D argument
9	Cudd_FirstPrime	Internal crash	id_000013	Same root cause as #4: different internal code path, crashes in Cudd_bddLeq
10	Cudd_SetVarMap	Cross-manager write	id_000032	See note below
11	Cudd_bddAnd	ZDD→BDD crash	id_000034	ZDD node passed to BDD operation: same systemic gap as #4 and #9

Notes Worth Flagging

Items #4, #9, #11 (ZDD→BDD confusion): All three involve passing ZDD nodes to BDD functions. Since all nodes share the same DdNode* type in C with no runtime type tag, this class of mistake is easy to make and impossible to catch at compile time. Type validation at BDD function entry points, even only in debug builds, would significantly improve robustness.

Item #6 (Cudd_SubsetWithMaskVars): ASAN detected an illegal free() on a pointer obtained from a struct field rather than a direct heap allocation. This suggests a memory management issue inside the library's own logic regardless of the input that triggered it, and may be worth investigating independently.

Item #10 (Cudd_SetVarMap): Causes an invalid memory write rather than a read, which is potentially more dangerous as it can silently corrupt data before any signal is raised.