Module haybale_pitchfork::secret [−][src]
Expand description
This module contains the dynamic taint-tracking layer implemented on
top of haybale. It provides a haybale::backend::Backend which
performs dynamic taint tracking and reports constant-time violations.
The BV, Memory, and Backend in this module are
intended to be used qualified whenever there is a chance of confusing
them with haybale::backend::{BV, Memory, Backend},
haybale::{cell_memory,simple_memory}::Memory, or boolector::BV.
Structs
A Backend which performs dynamic taint tracking and reports constant-time
violations.
This wrapper around Rc<Btor> exists simply so we can give it a different
implementation of haybale::backend::SolverRef than the one provided by
haybale::backend.
A Memory which tracks which of its contents are public or secret, and
reports constant-time violations whenever secret data is used as an address
for operations on it.
Enums
A wrapper around boolector::BV which can represent either public or secret
data.