diff --git a/examples/division-by-input.c b/examples/division-by-input.c new file mode 100644 index 0000000..f59affb --- /dev/null +++ b/examples/division-by-input.c @@ -0,0 +1,29 @@ +/* +Example in Bernhard Haslauer's Bachelor Thesis. +Input == #b00110000 (== 48 == '0') or +Input == #b00110010 (== 50 == '2') + */ + +uint64_t main() { + uint64_t a; + uint64_t* x; + + x = malloc(8); + *x = 0; + + read(0, x, 1); + + *x = *x - 48; + + // division by zero if the input was '0' (== 48) + a = 41 + (1 / *x); + + // division by zero if the input was '2' (== 50) + if (*x == 2) + a = 41 + (1 / 0); + + if (a == 42) + return 1; + else + return 0; +} \ No newline at end of file diff --git a/examples/eight-byte-input.c b/examples/eight-byte-input.c new file mode 100644 index 0000000..ca8b7a7 --- /dev/null +++ b/examples/eight-byte-input.c @@ -0,0 +1,19 @@ +// Example in Bernhard Haslauer's Bachelor Thesis. +// input "11111111" (8 '1's) lead to division by zero +uint64_t main() { + uint64_t a; + uint64_t* x; + + x = malloc(8); + *x = 0; + + read(0, x, 8); + + a = 3544668469065756977; + // input == "11111111" == 3544668469065756977 + if (*x == a) + *x = 42 / 0; + + return 0; +} + diff --git a/examples/memory-access.c b/examples/memory-access.c new file mode 100644 index 0000000..334b2a4 --- /dev/null +++ b/examples/memory-access.c @@ -0,0 +1,22 @@ +// Example in Bernhard Haslauer's Bachelor Thesis. +// invalid memory access if the input was '1' (== 49) or '2' (==50) +uint64_t main() { + uint64_t a; + uint64_t* x; + + x = malloc(8); + + *x = 0; + + read(0, x, 1); + + if (*x == 49) + // address outside virtual address space -> invalid memory access + *(x + (4 * 1024 * 1024 * 1024)) = 0; + if (*x == 50) + // address between data and heap -> invalid memory access + *(x + -2) = 0; + + return 0; +} + diff --git a/src/cli.rs b/src/cli.rs index 974716e..2686b42 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -77,6 +77,14 @@ pub fn args() -> Command { .default_value(DEFAULT_MEMORY_SIZE) .value_parser(value_parser_memory_size()), ) + .arg( + Arg::new("stdin") + .long("u8_stdin") + .help("Provides the first bytes for the stdin and allows to emulate \ + the inputs via arguments") + .value_name("BYTES") + .num_args(1..) + ) .arg( Arg::new("extras") .help("Arguments passed to emulated program") @@ -265,6 +273,13 @@ pub fn args() -> Command { .allow_hyphen_values(true) .num_args(1..) ) + .arg( + Arg::new("witness") + .help("enables witness extraction") + .short('w') + .long("witness") + .num_args(0) + ) ) .subcommand( Command::new("qubot") @@ -448,6 +463,13 @@ pub fn collect_arg_values(m: &ArgMatches, arg: &str) -> Vec { } } +pub fn collect_arg_values_as_usize(m: &ArgMatches, arg: &str) -> Vec { + match m.get_many::(arg) { + Some(iter) => iter.map(|it| it.parse::().unwrap()).collect(), + None => vec![], + } +} + fn value_parser_memory_size() -> clap::builder::RangedU64ValueParser { value_parser!(u64).range(1_u64..=1024_u64) } diff --git a/src/emulate.rs b/src/emulate.rs index 5a8360d..77d728b 100644 --- a/src/emulate.rs +++ b/src/emulate.rs @@ -24,6 +24,23 @@ pub struct EmulatorState { running: bool, stdin: Stdin, stdout: Stdout, + std_inputs: Vec, +} + +impl Clone for EmulatorState { + fn clone(&self) -> Self { + EmulatorState { + registers: self.registers.clone(), + memory: self.memory.clone(), + program_counter: self.program_counter, + program_break: self.program_break, + opened: Vec::new(), + running: self.running, + stdin: io::stdin(), + stdout: io::stdout(), + std_inputs: self.std_inputs.clone(), + } + } } impl EmulatorState { @@ -37,6 +54,7 @@ impl EmulatorState { running: false, stdin: io::stdin(), stdout: io::stdout(), + std_inputs: Vec::new(), } } @@ -50,6 +68,15 @@ impl EmulatorState { self.load_data_segment(program); self.load_stack_segment(argv); } + // The emulator reads from this vector instead of the Stdin when the + // read syscall (with file direction 0) is called in the emulated code. + // Will call the syscall again as soon the std_inputs is empty. + pub fn set_stdin(&mut self, inputs: Vec) { + self.std_inputs = inputs; + } + pub fn get_stdin(&self) -> &Vec { + &self.std_inputs + } // Partially prepares the emulator with the code segment from the // given `program`. This can be used in conjunction with other @@ -924,26 +951,33 @@ fn syscall_read(state: &mut EmulatorState) { let buffer = state.get_reg(Register::A1); let size = state.get_reg(Register::A2); - // Check provided address is valid, iterate through the buffer word - // by word, and emulate `read` system call via `std::io::Read`. - assert!(buffer & WORD_SIZE_MASK == 0, "buffer pointer aligned"); - let mut total_bytes = 0; // counts total bytes read - let mut tmp_buffer: Vec = vec![0; 8]; // scratch buffer - for adr in (buffer..buffer + size).step_by(riscu::WORD_SIZE) { - let bytes_to_read = min(size as usize - total_bytes, riscu::WORD_SIZE); - LittleEndian::write_u64(&mut tmp_buffer, state.get_mem(adr)); - let bytes = &mut tmp_buffer[0..bytes_to_read]; // only for safety - let bytes_read = state.fd_read(fd).read(bytes).expect("read success"); - state.set_mem(adr, LittleEndian::read_u64(&tmp_buffer)); - total_bytes += bytes_read; // tally all bytes - if bytes_read != bytes_to_read { - break; + if fd == 0 && !state.std_inputs.is_empty() { + for adr in (buffer..buffer + size).step_by(riscu::WORD_SIZE) { + let byte = state.std_inputs.pop().unwrap(); + state.set_mem(adr, byte as EmulatorValue); } - } - let result = total_bytes as u64; + } else { + // Check provided address is valid, iterate through the buffer word + // by word, and emulate `read` system call via `std::io::Read`. + assert!(buffer & WORD_SIZE_MASK == 0, "buffer pointer aligned"); + let mut total_bytes = 0; // counts total bytes read + let mut tmp_buffer: Vec = vec![0; 8]; // scratch buffer + for adr in (buffer..buffer + size).step_by(riscu::WORD_SIZE) { + let bytes_to_read = min(size as usize - total_bytes, riscu::WORD_SIZE); + LittleEndian::write_u64(&mut tmp_buffer, state.get_mem(adr)); + let bytes = &mut tmp_buffer[0..bytes_to_read]; // only for safety + let bytes_read = state.fd_read(fd).read(bytes).expect("read success"); + state.set_mem(adr, LittleEndian::read_u64(&tmp_buffer)); + total_bytes += bytes_read; // tally all bytes + if bytes_read != bytes_to_read { + break; + } + } + let result = total_bytes as u64; - state.set_reg(Register::A0, result); - debug!("read({},{:#x},{}) -> {}", fd, buffer, size, result); + state.set_reg(Register::A0, result); + debug!("read({},{:#x},{}) -> {}", fd, buffer, size, result); + } } fn syscall_write(state: &mut EmulatorState) { diff --git a/src/main.rs b/src/main.rs index 7dc0a80..384c365 100644 --- a/src/main.rs +++ b/src/main.rs @@ -27,7 +27,10 @@ use ::unicorn::disassemble::disassemble; use ::unicorn::emulate::EmulatorState; use anyhow::{Context, Result}; use bytesize::ByteSize; -use cli::{collect_arg_values, expect_arg, expect_optional_arg, LogLevel, SatType, SmtType}; +use cli::{ + collect_arg_values, collect_arg_values_as_usize, expect_arg, expect_optional_arg, LogLevel, + SatType, SmtType, +}; use env_logger::{Env, TimestampPrecision}; use riscu::load_object_file; use std::{ @@ -66,7 +69,11 @@ fn main() -> Result<()> { let argv = [vec![arg0], extras].concat(); let program = load_object_file(input)?; let mut emulator = EmulatorState::new(memory_size as usize); + let mut std_inputs = collect_arg_values_as_usize(args, "stdin"); + std_inputs.reverse(); + emulator.bootstrap(&program, &argv); + emulator.set_stdin(std_inputs); emulator.run(); Ok(()) @@ -96,14 +103,15 @@ fn main() -> Result<()> { let emulate_model = is_beator && args.get_flag("emulate"); let arg0 = expect_arg::(args, "input-file")?; let extras = collect_arg_values(args, "extras"); + let argv = [vec![arg0], extras].concat(); + let extract_witness = args.get_flag("witness"); let flag_32bit = args.get_flag("32-bit"); let mut model = if !input_is_dimacs { let mut model = if !input_is_btor2 { let program = load_object_file(&input)?; is64_bit = program.is64; - let argv = [vec![arg0], extras].concat(); generate_model( &program, memory_size, @@ -199,6 +207,7 @@ fn main() -> Result<()> { let mut emulator = EmulatorState::new(memory_size as usize); emulator.prepare(&program); // only loads the code load_model_into_emulator(&mut emulator, &model.unwrap()); + emulator.run(); return Ok(()); } @@ -215,10 +224,26 @@ fn main() -> Result<()> { if !discretize { replace_memory(model.as_mut().unwrap()); } - let gate_model = bitblast_model(&model.unwrap(), true, 64); + + let input = expect_arg::(args, "input-file")?; + let program = load_object_file(input)?; + let mut emulator = EmulatorState::new(memory_size as usize); + + if extract_witness { + emulator.bootstrap(&program, &argv); + } + + let gate_model = bitblast_model(model.as_ref().unwrap(), true, 64); if sat_solver != SatType::None { - solve_bad_states(&gate_model, sat_solver, terminate_on_bad, one_query)? + solve_bad_states( + &gate_model, + sat_solver, + terminate_on_bad, + one_query, + emulator, + extract_witness, + )? } if output_to_stdout { diff --git a/src/unicorn/bitblasting.rs b/src/unicorn/bitblasting.rs index a39be41..8ab4065 100644 --- a/src/unicorn/bitblasting.rs +++ b/src/unicorn/bitblasting.rs @@ -22,11 +22,20 @@ pub struct GateModel { pub mapping: HashMap>, // maps a btor2 operator to its resulting bitvector of gates pub mapping_adders: HashMap, pub constraint_based_dependencies: HashMap, // used or division and remainder, and when qubot whats to test an input (InputEvaluator). + pub witness: Option, +} + +#[derive(Debug, Eq, PartialEq)] +pub struct Witness { + pub name: String, + pub bad_state_gate: GateRef, + pub gate_assignment: HashMap, + pub input_bytes: Vec, } pub type GateRef = Rc>; -#[derive(Debug)] +#[derive(Debug, Eq, PartialEq)] pub enum Gate { ConstTrue, ConstFalse, @@ -1482,6 +1491,7 @@ impl<'a> BitBlasting<'a> { mapping: self.mapping, mapping_adders: self.mapping_adders, constraint_based_dependencies: self.constraint_based_dependencies, + witness: None, } } } diff --git a/src/unicorn/bitblasting_dimacs.rs b/src/unicorn/bitblasting_dimacs.rs index 572f4dd..ce2155d 100644 --- a/src/unicorn/bitblasting_dimacs.rs +++ b/src/unicorn/bitblasting_dimacs.rs @@ -90,6 +90,8 @@ impl CNFContainer for DimacsContainer { fn record_variable_name(&mut self, var: Self::Variable, name: String) { self.variable_names.push((var, name)); } + + fn record_input(&mut self, _var: Self::Variable, _gate: &GateRef) {} } impl DimacsWriter { diff --git a/src/unicorn/builder.rs b/src/unicorn/builder.rs index fef8edf..f466fc6 100644 --- a/src/unicorn/builder.rs +++ b/src/unicorn/builder.rs @@ -284,7 +284,7 @@ impl ModelBuilder { nid: self.current_nid, memory: self.memory_counter_node.clone(), address: address.clone(), - value: next_value_node.clone(), + value: next_value_node, }); self.memory_counter_flow = self.new_ite( diff --git a/src/unicorn/cnf.rs b/src/unicorn/cnf.rs index 8d1ab9a..4fdc69e 100644 --- a/src/unicorn/cnf.rs +++ b/src/unicorn/cnf.rs @@ -16,6 +16,7 @@ pub trait CNFContainer { fn new_var(&mut self) -> Self::Variable; fn add_clause(&mut self, literals: &[Self::Literal]); fn record_variable_name(&mut self, var: Self::Variable, name: String); + fn record_input(&mut self, var: Self::Variable, gate: &GateRef); } pub struct CNFBuilder { @@ -67,6 +68,10 @@ impl CNFBuilder { self.container.record_variable_name(var, name); } + fn record_input(&mut self, var: C::Variable, gate: &GateRef) { + self.container.record_input(var, gate); + } + #[rustfmt::skip] fn process(&mut self, gate: &GateRef) -> C::Variable { match &*gate.borrow() { @@ -83,6 +88,7 @@ impl CNFBuilder { Gate::InputBit { name } => { let gate_var = self.next_var(); self.record_variable_name(gate_var, name.clone()); + self.record_input(gate_var, gate); gate_var } Gate::Not { value } => { diff --git a/src/unicorn/dimacs_parser.rs b/src/unicorn/dimacs_parser.rs index f7d3631..3c6ff0b 100644 --- a/src/unicorn/dimacs_parser.rs +++ b/src/unicorn/dimacs_parser.rs @@ -103,6 +103,7 @@ impl DimacsParser { mapping: HashMap::new(), mapping_adders: HashMap::new(), constraint_based_dependencies: HashMap::new(), + witness: None, } } diff --git a/src/unicorn/sat_solver.rs b/src/unicorn/sat_solver.rs index 6c97ef2..d9d3458 100644 --- a/src/unicorn/sat_solver.rs +++ b/src/unicorn/sat_solver.rs @@ -1,19 +1,24 @@ -use crate::unicorn::bitblasting::{get_constant, or_gate, Gate, GateModel, GateRef}; +use crate::unicorn::bitblasting::{get_constant, or_gate, Gate, GateModel, GateRef, Witness}; use crate::unicorn::{Node, NodeRef}; use crate::SatType; use anyhow::{anyhow, Result}; -use log::{debug, warn}; +use log::{debug, trace, warn}; +use std::collections::HashMap; +use std::ops::Deref; +use std::panic; +use unicorn::emulate::EmulatorState; // // Public Interface // - #[allow(unused_variables)] pub fn solve_bad_states( gate_model: &GateModel, sat_type: SatType, terminate_on_bad: bool, one_query: bool, + emulator: EmulatorState, + extract_witness: bool, ) -> Result<()> { match sat_type { SatType::None => unreachable!(), @@ -22,18 +27,24 @@ pub fn solve_bad_states( gate_model, terminate_on_bad, one_query, + emulator, + extract_witness, ), #[cfg(feature = "varisat")] SatType::Varisat => process_all_bad_states::( gate_model, terminate_on_bad, one_query, + emulator, + extract_witness, ), #[cfg(feature = "cadical")] SatType::Cadical => process_all_bad_states::( gate_model, terminate_on_bad, one_query, + emulator, + extract_witness, ), } } @@ -41,11 +52,30 @@ pub fn solve_bad_states( // // Private Implementation // +#[should_panic] +fn emulate_witness(emulator: &mut EmulatorState, witness: Witness) { + println!( + "Emulating bad state {:?} with input {:?}:", + witness.name, + witness.input_bytes.clone() + ); + println!("---------------------------------------------------"); + emulator.set_stdin(witness.input_bytes); + let result = panic::catch_unwind(|| { + let mut emulator_clone: EmulatorState; + emulator_clone = emulator.clone(); + emulator_clone.run(); + }); + if result.is_ok() { + println!("Bad state {} did not produce expected panic.", witness.name); + } + println!("---------------------------------------------------\n"); +} #[allow(dead_code)] #[derive(Debug, Eq, PartialEq)] enum SATSolution { - Sat, + Sat(Option), Unsat, Timeout, } @@ -55,6 +85,55 @@ trait SATSolver { fn name() -> &'static str; fn prepare(&mut self, gate_model: &GateModel); fn decide(&mut self, gate_model: &GateModel, gate: &GateRef) -> SATSolution; + + fn print_witness(witness_ref: &mut Witness) { + let witness = &witness_ref.gate_assignment; + let mut input: HashMap> = HashMap::new(); + let mut start; + if witness.is_empty() { + println!("No witness produced for this bad state."); + return; + } + + for key in witness.keys() { + if let Gate::InputBit { name } = key.value.borrow().deref() { + // name = "1-byte-input[n=\d][bit=\d]" + // ^--- the 15th char + // assert: bit is explicit + start = name.find(']').unwrap(); + let n = name[15..start].parse().unwrap(); + let size = name.chars().next().and_then(|c| c.to_digit(10)).unwrap() as usize; + let mut bit: usize = name[start + 6..name.len() - 1].parse().unwrap(); + bit = size * 8 - 1 - bit; + + let bit_assignment = *witness.get(key).unwrap(); + if let Some(bits) = input.get_mut(&n) { + if let Some(bit_value) = bits.get_mut(bit) { + *bit_value = bit_assignment; + } else { + bits.resize(bit + 1, bit_assignment); + } + } else { + let mut bits: Vec = Vec::new(); + bits.resize(bit + 1, bit_assignment); + input.insert(n, bits); + } + } else { + panic!("Gates in the Witness must be Input Bit Gates."); + } + } + for bits in input { + let mut output = String::new(); + print!(" input at [n={}] ", bits.0); + + for bit in bits.1 { + output.push(if bit { '1' } else { '0' }); + } + let bits_as_int = usize::from_str_radix(&output, 2).unwrap(); + witness_ref.input_bytes.push(bits_as_int); + println!("{} {}", output, bits_as_int); + } + } } fn process_single_bad_state( @@ -64,18 +143,38 @@ fn process_single_bad_state( gate: &GateRef, terminate_on_bad: bool, one_query: bool, + (emulator, extract_witness): (&mut EmulatorState, bool), ) -> Result<()> { if !one_query { let bad_state = bad_state_.unwrap(); if let Node::Bad { name, .. } = &*bad_state.borrow() { + trace!( + "process_single_bad_state {}", + name.as_deref().unwrap_or("?") + ); let solution = solver.decide(gate_model, gate); match solution { - SATSolution::Sat => { + SATSolution::Sat(witness_opt) => { warn!( "Bad state '{}' is satisfiable ({})!", name.as_deref().unwrap_or("?"), S::name() ); + if extract_witness { + match witness_opt { + Some(mut witness) => { + witness.name = name.clone().unwrap(); + println!("Solution by {}: ", S::name()); + S::print_witness(&mut witness); + // TODO: flag for witness emulation + emulate_witness(emulator, witness); + } + None => { + println!("No Witness"); + } + } + } + if terminate_on_bad { return Err(anyhow!("Bad state satisfiable")); } @@ -97,7 +196,7 @@ fn process_single_bad_state( assert!(bad_state_.is_none()); let solution = solver.decide(gate_model, gate); match solution { - SATSolution::Sat => { + SATSolution::Sat(..) => { warn!("At least one bad state evaluates to true ({})", S::name()); } SATSolution::Unsat => { @@ -114,6 +213,8 @@ fn process_all_bad_states( gate_model: &GateModel, terminate_on_bad: bool, one_query: bool, + mut emulator: EmulatorState, + extract_witness: bool, ) -> Result<()> { debug!("Using {:?} to decide bad states ...", S::name()); let mut solver = S::new(); @@ -123,6 +224,7 @@ fn process_all_bad_states( .bad_state_nodes .iter() .zip(gate_model.bad_state_gates.iter()); + for (bad_state, gate) in zip { process_single_bad_state( &mut solver, @@ -131,7 +233,8 @@ fn process_all_bad_states( gate, terminate_on_bad, one_query, - )? + (&mut emulator, extract_witness), + )?; } } else { let mut ored_bad_states: GateRef; @@ -171,7 +274,8 @@ fn process_all_bad_states( &ored_bad_states, terminate_on_bad, one_query, - )? + (&mut emulator, extract_witness), + )?; } } @@ -181,10 +285,11 @@ fn process_all_bad_states( // TODO: Move this module into separate file. #[cfg(feature = "kissat")] pub mod kissat_impl { - use crate::unicorn::bitblasting::{GateModel, GateRef}; + use crate::unicorn::bitblasting::{Gate, GateModel, GateRef, HashableGateRef, Witness}; use crate::unicorn::cnf::{CNFBuilder, CNFContainer}; use crate::unicorn::sat_solver::{SATSolution, SATSolver}; - use kissat_rs::{AnyState, INPUTState, Literal, Solver}; + use kissat_rs::{AnyState, Assignment, INPUTState, Literal, Solver}; + use std::collections::HashMap; pub struct KissatSolver {} @@ -192,6 +297,7 @@ pub mod kissat_impl { current_var: i32, solver: Solver, state: Option, + variables: HashMap, } impl CNFContainer for KissatContainer { @@ -200,10 +306,12 @@ pub mod kissat_impl { fn new() -> Self { let (solver, state) = Solver::init(); + Self { current_var: 1, solver, state: Some(state), + variables: HashMap::new(), } } @@ -234,6 +342,14 @@ pub mod kissat_impl { fn record_variable_name(&mut self, _var: Literal, _name: String) { // nothing to be done here } + + fn record_input(&mut self, var: Self::Variable, gate: &GateRef) { + if let Gate::InputBit { name } = &*gate.borrow() { + if name.len() > 1 && name[1..].starts_with("-byte-input") { + self.variables.insert(var, gate.clone()); + } + } + } } impl SATSolver for KissatSolver { @@ -248,7 +364,6 @@ pub mod kissat_impl { fn prepare(&mut self, _gate_model: &GateModel) { // nothing to be done here } - fn decide(&mut self, gate_model: &GateModel, gate: &GateRef) -> SATSolution { let mut builder = CNFBuilder::::new(); @@ -267,8 +382,32 @@ pub mod kissat_impl { let cnf = builder.container_mut(); let state = cnf.state.take().unwrap(); + let literals = cnf.variables.keys(); + match cnf.solver.solve(state).unwrap() { - AnyState::SAT(..) => SATSolution::Sat, + AnyState::SAT(sat_state) => { + let mut witness = Witness { + name: String::new(), + bad_state_gate: gate.clone(), + gate_assignment: HashMap::new(), + input_bytes: vec![], + }; + let mut sat = sat_state; + for literal in literals.copied() { + let value = cnf.solver.value(literal, sat).unwrap(); + let assignment = match value.0 { + Assignment::True => true, + Assignment::False => false, + Assignment::Both => false, + }; + sat = value.1; + let gate_ref = cnf.variables.get(&literal).cloned(); + witness + .gate_assignment + .insert(HashableGateRef::from(gate_ref.unwrap()), assignment); + } + SATSolution::Sat(Some(witness)) + } AnyState::UNSAT(..) => SATSolution::Unsat, AnyState::INPUT(..) => panic!("expecting 'SAT' or 'UNSAT' here"), } @@ -325,6 +464,11 @@ pub mod varisat_impl { fn record_variable_name(&mut self, _var: Var, _name: String) { // nothing to be done here } + + #[allow(unused_variables)] + fn record_input(&mut self, var: Self::Variable, gate: &GateRef) { + todo!() + } } impl SATSolver for VarisatSolver<'_> { @@ -351,7 +495,7 @@ pub mod varisat_impl { let bad_state_lit = VarisatContainer::var(bad_state_var); self.builder.container_mut().solver.assume(&[bad_state_lit]); match self.builder.container_mut().solver.solve().unwrap() { - true => SATSolution::Sat, + true => SATSolution::Sat(None), false => SATSolution::Unsat, } } @@ -411,6 +555,11 @@ pub mod cadical_impl { fn record_variable_name(&mut self, _var: i32, _name: String) { // nothing to be done here } + + #[allow(unused_variables)] + fn record_input(&mut self, var: Self::Variable, gate: &GateRef) { + todo!() + } } impl SATSolver for CadicalSolver { @@ -445,7 +594,7 @@ pub mod cadical_impl { .solver .solve_with([bad_state_lit].iter().copied()) { - Some(true) => SATSolution::Sat, + Some(true) => SATSolution::Sat(None), Some(false) => SATSolution::Unsat, None => SATSolution::Timeout, } diff --git a/theses/README.md b/theses/README.md index fc67f9d..e0875fb 100644 --- a/theses/README.md +++ b/theses/README.md @@ -1,5 +1,15 @@ # Bachelor Theses on Unicorn +## Witness Extraction and Validation in Unicorn by Bernhard Haslauer, University of Salzburg, Austria, 2024 ([PDF](https://github.com/cksystemsgroup/unicorn/blob/main/theses/bachelor_thesis_haslauer.pdf), [Release](https://github.com/cksystemsgroup/unicorn/commit/ebbe6feca5a17438cb82da21712e08517d2b4db4)) + +Unicorn, a toolchain for symbolic execution, was previously limited to evaluating only whether a given machine code could run into an error state without providing the corresponding inputs for such a case. +To determine these inputs, a series of steps with external tools have to be run through. +This Bachelor's thesis explores the possibility of incorporating this feature directly into Unicorn, with the objective of improving Unicorn's capabilities in generating and validating the inputs for these errors states. +With this proposed extension, Unicorn can extract the inputs and feed them into its built-in RISC-V emulator to validate if these inputs indeed induce the expected errors. +If the inputs are accurate, the emulator encounters the predicted errors. +In addition, this thesis provides an insight into the concepts used as well as details about the implementation. + + ## 32-bit Support for Bit-Precise Modeling of RISC-U Code by Patrick Weber, University of Salzburg, Austria, 2024 ([PDF](https://github.com/cksystemsgroup/unicorn/blob/main/theses/bachelor_thesis_weber.pdf),[Release](https://github.com/cksystemsgroup/unicorn/commit/1d77ed2dac08f1263d4f5f21a3b84a84047cacb8)) This thesis presents the 32-bit support for Unicorn, a symbolic execution engine for bit-precise modeling of RISC-V code. The primary motivation for this development was to improve the engine’s performance and extend its capabilities diff --git a/theses/bachelor_thesis_haslauer.pdf b/theses/bachelor_thesis_haslauer.pdf new file mode 100644 index 0000000..f65dd18 Binary files /dev/null and b/theses/bachelor_thesis_haslauer.pdf differ