---
# System prepended metadata

title: BA Meeting Notes

---

# BA Meeting Notes

## Meeting 2020-11-06

- Automatic detection of common patters of memory-safety vulnerbilities
    - Reference: paper Xu2020
    - Use-After-Free (section 4.3)
        - Unsafe Constructor with Temporary Buffer
            - return value constructed from raw pointer to local which will be dropped upon returning
            - e.g. CVE-2019-16140 (code example 12)
            - ```rust
              fn from(buffer: Buffer) -> Vec<u8> {
                  let mut slice = Buffer::allocate(buffer.len);
                  let len = buffer.copy_to(&mut slice);
                  unsafe {
                      Vec::from_raw_parts(slice.as_mut_ptr(), len, slice.len());
                  }
              }
              ```
            - fix: make slice ManuallyDrop or call mem::forget
        - Dropping Uninitialized Memory
            - caused by using mem::uninitialized or Vec::set_len and initialization code which may error or panic
            - fix: use MaybeUninit or guarantee that initialization never fails
            - problem for automatic detection: when does the memory count as initialized?
            - see code examples 14 and 15 in paper
    - Double-Free
        - Shared Mutable Aliases without ManuallyDrop
            - fix: use ManuallyDrop on all but one alias
        - Enforcing ManuallyDrop Too Late
            - the program may panic before mem::forget is called
        - Buffer Shrinking Too Late
- Detection of Integer Overflows
    - arithmetic operations may overflow since checks are disabled by default in release builds
    - discussion on Zulip: https://rust-lang.zulipchat.com/#narrow/stream/146229-wg-secure-code/topic/unchecked.20arithmetic
    - if it is unclear if wrapping behaviour was intended overflows should be treated as potential sources for bugs
        - disambiguate intended behaviour by using checked_ or wrapping_ methods
    - automatic detection by symbolic execution seems feasible
        - which representation of the source code should the analyzer operate on?
            - LLVM IR
                - previous work by haybale, cargo klee
                - might be missing crucial information (signedness?)
            - MIR
                - experimental support for overflow checks in prusti
            - higher levels (HIR)
                - probably missing type information
    - interation with memory-safety: under which circumstances do integer overflows lead to memory-safety vulnerbilities (e.g. buffer overflows)
        - interesting but harder to reason about
        - example case: CVE-2018-1000810
        - ```rust
          let mut buf = Vec::with_capacity(self.len() * n);
          unsafe {
              ptr::copy_nonoverlapping(buf.as_ptr(), (buf.as_mut_ptr() as *mut T).add(buf.len()), buf.len());
          }
          ```

## Meeting 2020-11-10

- Definition of integer overflows in the rust [reference](https://doc.rust-lang.org/reference/expressions/operator-expr.html#overflow)
- Symbolic execution for finding integer overflows
    - Prusti
        - enable integer overflow checks with PRUSTI_CHECK_BINARY_OPERATIONS=true [wiki](https://github.com/viperproject/prusti-dev/wiki/tutorial#overflow-checks)
        - adds checks after each binary operation to check for overflows [code](https://github.com/viperproject/prusti-dev/blob/6b98dd551b29fc1b6ec762e95e58158affde4564/prusti-viper/src/encoder/mir_encoder.rs#L499)
        - encodes integer types with bounds check [code](https://github.com/viperproject/prusti-dev/blob/6b98dd551b29fc1b6ec762e95e58158affde4564/prusti-viper/src/encoder/type_encoder.rs#L223)
    - KLEE
        - [guide](https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-klee.md)
        - compile with -Coverflow-checks=yes rustflag to ensure runtime checks (in release mode)
            - KLEE will abort on panic
        - steps (automated by [cargo-verify](https://github.com/project-oak/rust-verification-tools/blob/main/scripts/cargo-verify) script)
            1. compile rust to LLVM IR or bitcode
            2. call klee on bitcode
            3. interprete .ktest output files
            4. replay with specific values
        - problem: wrapper code
            - specify symbolic variables
            - reject invalid values (e.g. non-existant enum values)
            - print out concrete values when replayed
            - requires FFI bindings to KLEE (e.g. [verification-annotations](https://github.com/project-oak/rust-verification-tools/blob/main/docs/using-annotations.md))
            - higher level abstractions exist (propverify: testing based approach)
        - ideally: run analysis without modifications to the code

## Meeting 2020-11-23
- exposé needs more work
- problem space x solution space matrix
- orthogonal vs layered goals

## Meeting 2020-11-26
- implement own symbolic execution engine vs build on top of KLEE etc.
- outline solution tasks in more detail
- schedule
    - parallel implementation and writing tasks

## Meeting 2020-12-02
- Pending registration (deadline 08.12.2020)
- Schedule
    - correct time estimates
    - address Related Work earlier
        - compare own approach with similar approaches (-> evaluation)
        - define novelty by differentiating from related but different approaches
    - only basic set of code samples
        - test on corner cases later
- evaluation criteria
    - change order (usefulness first)
    - rename applicability to robustness
        - termination
        - exit with result or reason why analysis was not possible
        - distingish no results from incomplete analysis
    - performance
        - also evaluate scalability
- next steps
    - research symex engines operating on the MIR (until 9.12.)
        - crux (converts MIR to JSON, written in Haskell)
        - Viper (back-end of Prusti)
    - decide on a engine (until 16.12.)
- weekly meetings Wed. 15:30

## Meeting 2020-12-09
- Approaches for SymEx on the MIR
    - Crux
        - basic architecture: mir-json -> crux-mir -> crux -> crucible -> what4 -> solver (eg. z3)
        - [mir-json](https://github.com/GaloisInc/mir-json)
            - written in Rust
            - provides cargo subcommand `crux-test`
            - uses the Rust compiler as a library (`rustc_driver::run_compiler`)
                - => bound to a specific compiler version
            - translates MIR into JSON representation
            - "links" JSON of multiple crates together
                - causes bug
        - [crux-mir](https://github.com/GaloisInc/crucible/tree/master/crux-mir)
            - written in Haskell
            - contains alternative Rust sources for standard libs (libcore, libc, libstd)
                - adds "hooks" for later processing
                - e.g. [original](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/mod.rs#L92) vs [modified](https://github.com/GaloisInc/crucible/blob/master/crux-mir/lib/libcore/slice/mod.rs#L73)
                - also constrains rust version
                - additionally provides API for crux/crucible
                    - [assert](https://github.com/GaloisInc/crucible/blob/master/crux-mir/lib/crucible/lib.rs#L56), assume, symbolic
                    - more complex symbolic Types (symbolic array), specific to engine
            - important files
                - `src/Mir/Language.hs`
                    - main entry point
                    - integrates with crux
                - `src/Mir/Generate.hs`
                    - `gnerateMIR`: calls mir-json
                    - `translateMIR`: translate to crucible CFG
                - `src/Mir/TransCustom.hs`
                    - replace hooked functions with specialized implementations
                        - encodes safety checks [src](https://github.com/GaloisInc/crucible/blob/master/crux-mir/src/Mir/TransCustom.hs#L582) 
                - `src/Mir/Overrides.hs`
                    - replace intrinsic functions (assert, assume)
                - `src/Mir/Pass/*`
                    - mir-to-mir AST transformations
        - could not test, mir-json fails (presumably) when deserializing metadata [link](https://github.com/GaloisInc/mir-json/blob/master/src/lib_util.rs#L361)
            - existing [bug report](https://github.com/GaloisInc/crucible/issues/578)
        - building on crux would already solve some of the challanges, remaining tasks:
            - change entry point for symbolic execution (autogenerate function calls instead of [crux-test])
            - improve detection of unsoundness
    - Prusti
        - written in Rust, split into multiple crates
        - directly inegrates with the Rust compiler [src](https://github.com/viperproject/prusti-dev/blob/master/prusti/src/driver.rs#L203)
        - translates MIR into Viper language [tutorial](https://viper.ethz.ch/tutorial/)
            - encodes type bounds [src](https://github.com/viperproject/prusti-dev/blob/master/prusti-viper/src/encoder/type_encoder.rs)
        - interfaces with the Viper engine over JNI
            - high level rust bindings exist [link](https://github.com/viperproject/prusti-dev/tree/master/viper)
        - API seems focused around verification, use for SymEx without verification unclear
    - Seer (based on Miri)
        - fork of Miri
        - incomplete and unmaintained
        - discussion of symbolic execution in Miri
            - [link](https://github.com/rust-lang/miri/issues/440#issuecomment-532146161)
    - Challenges of operating on the MIR
        - obtaining the MIR of std and other crates
        - each translation is an additional source of bugs
    - next steps:
        - try to get crux running
        - ask Prusti developers about potential for SymEx
        - evaluate LLVM based engines (-> KLEE)

## Meeting 2020-12-16
- crux
    - works in the Docker container
    - does not support [symbolic length](https://github.com/GaloisInc/crucible/blob/c1da81f05e7a8ac80787e2f161ba341a312a6302/crux-mir/src/Mir/Intrinsics.hs#L1462)
- klee
    - RUSTFLAGS: `-Clto -Cembed-bitcode=yes --emit=llvm-bc -Cpanic=abort`
    - panic caused by runtime checks -> unit test coverage might not trigger panic
    - two wrappers
        - cargo-klee
            - cargo integration
            - very simple
            - no_std, custom panic_handler
        - rust-verification-tools
            - cargo-verify python script
            - allows selecting unit tests as entry points (demangling!)
    - problems
        - klee does not support sse
            - can't be safely disabled in rustc [link](https://doc.rust-lang.org/rustc/targets/known-issues.html)
            - TODO test on real-world crates
        - only finds one issue at a time
            - maybe klee continues if it detects an overflow instead of a panic
        - how to do MIR to MIR transformation?

## Meeting 2021-01-07

- Concretized problem: Find integer overflows which affect the size of an allocation
    - Real world instances
        - [CVE-2018-1000810](https://rustsec.org/advisories/CVE-2018-1000810.html)
            - overflow in multiplication
            - allocation with Vec::with_capacity
            - unsoundness in ptr::copy_nonoverlapping
        - [RUSTSEC-2019-0033](https://rustsec.org/advisories/RUSTSEC-2019-0033.html)
            - overflow in `usize::next_power_of_two()`
            - allocation with Vec::with_capacity
            - no immediate unsoundness but DOS can be caused by same issue
- Idea from ELAID paper: combine symbolic execution with data flow analysis
    - Two options
        - First symbolic execution, then data flow
        - First data flow, then symex
    - Use first analysis to achieve good coverage (minimize false negatives) and second analysis to filter results (minimize false positives)
    - it seems easier to achieve coverage with data flow
        - path explosion issue less severe with data flow
        - data flow more lightweight (less state to track)
        - assumption: paths between int-overflow and alloc usually short
    - use symbolic execution as a filter
        - problem changes from complete coverage to line reachability
        - allows to employ directed symbolic execution
        - abort when target instruction was reached
- Program Components
    - Data Flow Sink Identification
        - Inputs: Rust program
        - Output: Set of allocation calls (LLVM instructions)
    - (Backwards) data flow to integer operation (DF)
        - Inputs: sinks (alloc instructions)
        - Output: Set of potentially dangerous integer operations (LLVM instructions)
    - Overflow filter (OF)
        - Input: Set of potentially dangerous integer operations
        - Output: Set of likely dangerous interger operations
    - line reachability analysis (LRA)
        - Input: single instruction, analysis origin
        - Output: is instruction reachable?, satisfiying inputs
    - OF invokes LRA for each potentially dangerous integer operation
        - analysis origin is chosen to be containing or calling function
            - ELAID paper claims this to be sufficient
            - multiple calling funtions?
        - operation may overflow iff runtime check panic reachable
            - benefit: no need to distinguish signed and unsigned arithmetic
        - LRA should also check whether overflow path reaches alloc
- Implementation
    - Perform all analysis on the LLVM IR
        - no obvious need or benefit of another representation (MIR)
        - single representation: less translation between code locations
    - First implement LRA
        - are existing tools available?
        - modify haybale
    - Then implement DF, OF

## Meeting 2021-01-13

- revised concept: https://hackmd.io/6f71qDYES56FMyWf_CesSQ
- can data flow be inferred from the SMT representation of the allocation size parameter?
- how to distinguish signed and unsigned arithmetic in the LLVM IR?
    - signed and unsigned overflow are distinct (unsigned: ff->00, signed: 7f->80)
    - trigger both with 7f+81=00 127+(-127)=0, ff+81=80 (-1)+(-127)

## Meeting 2021-01-20

- state of implementation
    - tracking of unsigned integer overflows in haybale works
    - tested on some basic examples
- implementation of dataflow analysis
    - first implement intraprocedual analysis with fixpoint iteration
    - later on a interprocedual analysis is probably required
        - we want to check with constraints from calling functions
        - alloc, overflowing op in repeat, but safety controlled by calling functions
- next steps
    - implement intraprocedural dataflow
    - test whether analysis scales to larger crates
        - rand, http
        - how to combine multiple modules?
    - outline thesis structure
        - collect good points for discussion

## Meeting 2021-01-27

- thesis [outline](https://gitlab.cc-asp.fraunhofer.de/ba-stolz/thesis/-/blob/master/outline.md)
- Interesting points to discuss in thesis
    - MIR vs LLVM IR
        - MIR
            + closer to source code
            + type information
            - not stable, might change between Rust releases
            - more complex structure
        - LLVM IR
            + simpler structure, less features to support
            + build upon results from KLEE etc.
            - additional translation steps may introduce bugs
            - missing information (signedness)
    - Implement symex from scratch vs using existing tools
        - from scratch
            + operate directly on the MIR without further translation
            + integrate dataflow directely
        - existing tools
            + many edge cases already covered
            + focus more on application for vuln detection
    - KLEE vs Haybale
        - KLEE
            + performant (state representation)
            + good support for integer overflows
            + (partially) models environment symbolically
            - hard to adapt / integrate with
        - Haybale 
            - written in Rust, smaller, easier to adapt
            - not very optimized (stack overflow when used on lto output)
            - no out-of-the-box support for detecting interger overflows
    - DF -> SymEx vs SymEx -> DF
        - DF first
            + easier to achieve good coverage
            + SymEx can be used as a filter
        - SymEx first
            + DF might not be required if it can be inferred from symbolic representation
            - path explosion issue more severe
    - DF Direction
    - DF, SymEx on same representation
        - same representation
            + no extra translation between code locations required
        - different representations
            + leverage advantages of each repr
    - Choice of DF Sinks
        - few sinks (lower level)
            + catch more allocations
            - DF must traverse deeper call hierarchy
        - more sinks (higher level)
            + closer to size calculations, shorter paths
            - might miss allocations
    - Choice of SymEx Origin
        - closer to allocation
            + fewer paths to explore
            - caler constraints missing -> false postivies
        - public API
            + precision
            - more branching
- From the Rust community
    - https://github.com/rust-lang/rust/issues/76579
    - https://internals.rust-lang.org/t/pre-rfc-extending-where-clauses-with-limited-formal-verification/13791

## Meeting 2021-02-03

## Meeting 2021-02-10 (skipped)

## Meeting 2021-02-17 (skipped)

## Meeting 2021-02-24

- new integer undeflow vulnerability in `std`: [#82282](https://github.com/rust-lang/rust/issues/82282)
- Implementation TODOs
    - implement cargo subcommand
        - [cargo reference](https://doc.rust-lang.org/cargo/reference/external-tools.html#custom-subcommands)
        - steps:
            - call
              ```
              cargo rustc --message-format=json -- --emit=llvm-bc -Cpanic=abort -Coverflow-checks=off
              ```
            - parse json output using [cargo metadata](https://crates.io/crates/cargo_metadata) to get names of generated bitcode files (LLVM module)
            - run analyzer on each module
            - print results
        - benefit: faster testing
    - support more types of overflow
        - division / modulo by -1 requires signed arithmetic
    - handle signed and unsigned arithmetic -> impl chapter
        - approach: use debug info, propagate (forward DF?)
        - issues: parse metadata in llvm-ir crate
    - find symex entrypoints
        - approach: use public API as orientation
        - rustdoc json output (`rustdoc -w json`)
        - currently: go up n levels in call graph from sinks 
    - support indirect calls in DF analyis (e.g. trait objects)
        - probably rather hard, maybe only support some common cases
- Evaluation TODOs
    - extract std vulnerability into self-contained test case
    - extract parts of std collections
    - run on more popular crates
    - current problem:
        - haybale struggles with larger projects
        - possible solutions:
            - smater selection of symex sources
            - abort symex after reaching sinks? probably not
            - overapproximate calls to certain library functions
    - formulate concrete scenarios for evaluation criteria from expos´e*
        - measure scalability
- Writing TODOs
    - finish detailed structure of problem statement and approach
    - begin structuring implementation
        - signed, unsigned (disadvantages )

## Meeting 2021-03-03

- Signed / Unsigned differentiation harder than expected
    - metadata not implemented in `llvm-ir` crate
    - even with metadata: non-trivial to link types to variables
    - alternatives
        - compile with overflow checks, skip actual check somehow
        - current solution: consider either as overflow, overapproximates but simple and reliable
- Should truncation always be consideres as "overflow"?
- Evaluation strategy
    - Accuracy
        - run analysis on real-world and contrived examples with known result
        - results should be:
            - comprehensive: detect as many cases as possible
            - relevant: detected cases are actually interesting
            - precise: each detected issue should pinpoint its cause as precisely as possible -> usability
        - real-word examples
            - [`CVE-2018-1000810`](https://rustsec.org/advisories/CVE-2018-1000810.html): std::str::repeat, motivating example
            - [`RUSTSEC-2019-0033`](https://rustsec.org/advisories/RUSTSEC-2019-0033.html): http, overflows next_power_of_two, causes infinite loop (-> DoS)
        - analyze crates that use vulnerable functions
            - how to find such crates?
        - designed test cases
            - different types of overflow
            - (different types of sinks (alloc functions))
            - edge cases
                - test overflow and symex sperately
                    - dataflow
                        - inter-, intraprocedural
                        - branching, loops
                - overflow makes dataflow impossible
                - dataflow only possible in case of overflow
    - Robustness
        - fail in a controlled manner
        - handle unsupported code gracefully
        - test scenarios
            - code containing unsupported features
                - trait objects, recursive functions
                - should warn about possibly incomplete analysis
                - analyze unaffected code normally
            - complex code (lots of unsafe Rust)
                - std data structures (VecDeque, BTree)
                - [Juliet Testsuite](https://samate.nist.gov/SRD/testsuite.php)
                - three possible outcomes
                    - failure -> why did it fail?
                    - no results -> inconclusive
                    - some results -> verify manually
    - Scalability
        - bahavior of symbolic execution with increasingly more complex code
            - measure execution time, number of paths explored
        - effect of different sink choices
            - how much does choosing a lower level function as sink affect the performance of the analysis
        - what are the main factors influencing performance?

## Meeting 2021-03-10

- Writing
    - where to put CVE example?
    - definitions: critical, misbehaved
    - soundness requirement
    - approach graphic
- Evaluation
    - Test Cases
        - Dataflow: verify set of taints against expected result
            - intraprocedural
                - single basic block
                - mutiple basic blocks, only forward edges
                - multiple basic blocks, backward edges (loops)
            - interprodcedural
                - one sink function, two callers
                - two sink functions, one caller
                - deep call hierarchies, (3-10)
                - recursion
        - SymEx: verify set of overflows against expected result
            - assumption: haybale works correctly
            - different types of overflow
                - add, sub, mul over-, underflow
                    - only signed, only unsigned
                - signed div, rem
                - shift
                - signed unary minus
                - truncation
            - haybale [parameters](https://docs.rs/haybale/0.6.3/haybale/config/struct.Config.html#fields)
                - loop_bound
                - max_callstack_depth
                - solver_query_timeout
        - Combined: verify set of dangerous numeric operations against expected result
            - Juliet
                - CWE-680: 989 C, C++ samples
                - flow types: [page 37](https://samate.nist.gov/SARD/resources/Juliet_Test_Suite_v1.2_for_C_Cpp_-_User_Guide.pdf)
            - overflow makes dataflow impossible (path must reach allocation call)
              ```rust
              pub fn overflow_xor_dataflow(x: usize) -> Vec<Foo> {
                let a = x + 1;
                if x == 0 {
                    Vec::with_capacity(a)
                } else {
                    Vec::with_capacity(3)
                }
              }
              ```
              - this is why we need to branch on overflow
                  - possibly substatial performance benefit if we didn't do that (config option?)
            - dataflow only possible in case of overflow (cannot assume that op did not overflow)
              ```rust
              pub fn f3(x: usize) -> Vec<Foo> {
                let a = x + 1;
                if x == usize::MAX {
                    Vec::with_capacity(a)
                } else {
                    Vec::with_capacity(3)
                }
              }
              ```
            - multiple overflows
              ```rust
              pub fn f3(x: usize) -> Vec<Foo> {
                let a = x + 1;
                let b = x + 2;
                if x == usize::MAX {
                    Vec::with_capacity(a)
                } else {
                    Vec::with_capacity(3)
                }
              }
              ```
              
## Meeting 2021-03-17
- Writing
    - [current pdf](https://gitlab.cc-asp.fraunhofer.de/ba-stolz/thesis/-/blob/master/build/main.pdf)
- Implementation
    - allocation functions
        - HashMap::with_capacity
            - HashSet::with_capacity
        - Vec::with_capacity
            - String
            - BinaryHeap
            - OsString, PathBuf
            - BufReader, BufWriter, LineWriter
        - RawVec::with_capacity, RawVec::with_capacity_in
            - Vec::with_capacity
            - VecDeque
    - symex sink inaccurate
        - only checks if any sink reached
- Evaluation
    - Dataflow
        - [test cases](https://gitlab.cc-asp.fraunhofer.de/ba-stolz/llvm-ir-dataflow/-/blob/master/tests/bcfiles/dataflow.rs)
        - [preliminary results](https://gitlab.cc-asp.fraunhofer.de/ba-stolz/llvm-ir-dataflow/-/blob/master/tests/dataflow_test.rs)
            - currently issues with data structures (likely cause: bitcast instruction)
    - SymEx
        - [basic test cases](https://gitlab.cc-asp.fraunhofer.de/ba-stolz/haybale/-/blob/overflow-analysis/tests/bcfiles_overflow/ops.rs)
        - [preliminary results](https://gitlab.cc-asp.fraunhofer.de/ba-stolz/haybale/-/blob/overflow-analysis/tests/overflow_tests.rs)
    - Combined
        - debug info causes x10 increase in runtime
            - simpler debug info?

```
; dataflow::flow_array_inout
; Function Attrs: nounwind nonlazybind
define void @_ZN8dataflow16flow_array_inout17hc77ed2f9a2c1c274E(i32 %a) unnamed_addr #1 !dbg !634 {
start:
  %b = alloca [1 x i32], align 4
  %0 = bitcast [1 x i32]* %b to i32*, !dbg !635
  store i32 %a, i32* %0, align 4, !dbg !635
  %1 = getelementptr inbounds [1 x i32], [1 x i32]* %b, i64 0, i64 0, !dbg !636
  %_5 = load i32, i32* %1, align 4, !dbg !636
; call dataflow::sink
  call void @_ZN8dataflow4sink17h8419b97bfee5f129E(i32 %_5), !dbg !637
  br label %bb1, !dbg !637

bb1:                                              ; preds = %start
  ret void, !dbg !638
}
```

```
; dataflow::intra_match
; Function Attrs: nounwind nonlazybind
define void @_ZN8dataflow11intra_match17hb57095e388a57a58E(i32 %a, i32 %b, i32 %c) unnamed_addr #1 !dbg !1361 {
start:
  %c.dbg.spill = alloca i32, align 4
  %b.dbg.spill = alloca i32, align 4
  %a.dbg.spill = alloca i32, align 4
  %0 = alloca {}, align 1
  store i32 %a, i32* %a.dbg.spill, align 4
  call void @llvm.dbg.declare(metadata i32* %a.dbg.spill, metadata !1365, metadata !DIExpression()), !dbg !1368
  store i32 %b, i32* %b.dbg.spill, align 4
  call void @llvm.dbg.declare(metadata i32* %b.dbg.spill, metadata !1366, metadata !DIExpression()), !dbg !1369
  store i32 %c, i32* %c.dbg.spill, align 4
  call void @llvm.dbg.declare(metadata i32* %c.dbg.spill, metadata !1367, metadata !DIExpression()), !dbg !1370
  switch i32 %a, label %bb1 [
    i32 0, label %bb2
    i32 1, label %bb4
  ], !dbg !1371
```

## Meeting 2021-03-24 (async)

- Formalities
    - thesis title: *unsafe* numeric operations, but in thesis: *dangerous* numeric operations
        - can/should the title be changed?
    - when/how should the implementation be submitted?
        - at thesis deadline or before presentation?
- Dataflow with Pointers (problem from last week)
    - current rules
        - `store %val, %ptr`
            - taint `%val` if `%ptr` is tainted
        - `%val = load %ptr`
            - taint `%ptr` if `%val` is tainted
        - works for simple cases
            - ```
              store %a, %p
              %b = load %p
              call sink(%b)
              ```
            - correclty taints `%a`
    - problem: pointer aliasing
        - aliases created with
            - `%p2 = bitcast %p1`
            - `%p2 = getelementpointer %p1`
        - breaks this example
            - ```
              %p2 = bitcast %p1
              store %a, %p2
              %b = load %p1
              call sink(%b)
              ```
            - does not taint `%a`
        - possible fix: compute alias matrix beforehand
            - alias matrix determines if two variables are aliases
            - initialize with `bitcast` and `getelementpointer` instructions
            - when tainting a pointer: also taint its aliases

## Meeting 2021-03-31

- Other ways to create pointer aliases (besides `bitcast` and `getelementptr`)
    - `addrspacecast` instruction
        - easy (can be detected like `bitcast`), quite uncommon
    - convert pointer to integer (`ptrtoint`) and back (`inttoptr`)
        - hard, would require reasoning about flow between these instructions
    - aliases are created in function `%p2 = call foo(%p1)`
        - hard, would require propagating alias matrix inter-procedurally
- lifetime, flow sensitivity of pointers
    - example: `%x` should not be tainted
        - ```
          %p3 = bitcast %p1
          store %x, %p3
          %p2 = bitcast %p1
          store %a, %p2
          %b = load %p1
          call sink(%b)
          ```
    - solution: in `store %a, %p2` un-taint `%p2` and its aliases `%p1`, `%p3`
        - the previous value is overwritten
        - in principle, no reason why taints can not be removed
        - however, in for the basic approach it is assumed that taints are only added to be able to ensure termination
- to what extend can the guarantees from Rust's borrow checker be used?
    - Rust only allows immutable aliases