# 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)

              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)

              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

              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