---
title: Talk slides template
tags: Templates, Talk
description: View the slide with "Slide Mode".
---

# A few notes on call graphs & libsignal/rust

<!-- Put the link to this slide here so people can follow
slide: https://hackmd.io/p/template-Talk-slide -->

---
## Some numbers about libsignal/rust

- 480 files
- 37493 definitions
- 4555 functions
- 8207 calls

---

## The call graph for libsignal/rust

- [a huge call graph, to download and open with firefox](https://drive.google.com/file/d/1f6aTa41PwrF6j6QuExMWktzRxuEkxvpO/view?usp=sharing)

---

## Bottom-up approach

- given the stats for `libsignal/rust`, a bottom-up approach to verification, like starting from the call graph seems difficult

[The misguided quest for mechanistic AI interpretability](https://www.ai-frontiers.org/articles/the-misguided-quest-for-mechanistic-ai-interpretability) noted something somewhat similar:
> Meteorologists do not try to predict the weather by tracing every single molecule in the atmosphere, for instance. Similarly, it would be intractable to understand biological systems by starting from subatomic particles and working up from there.

## Top-down approach

Always with compositionality in mind,
- a top-down approach seems more feasible:
- start at modules level:

generated with `cargo depgraph --build-deps --dedup-transitive-deps --workspace-only | dot -Tpng > libsignal_workspace_deps.png`
- one could use also `cargo modules dependencies --package libsignal-protocol | xdot -` in a given crate like for instance, in this case, `libsignal-protocol`

---

## Choose a module to focus on

Say it's `libsignal-protocol`

---

## Display call graph filtered wrt a given file


---

## Display call graphs filtered wrt multiple files

- already challenging to navigate for 2 files:

---

## Display call graphs filtered wrt function names

- starting from `group_decrypt`

---

## Reachable states

- find a way to compute/approximate the reachable states starting from a given initial state and a function
- identified Kani, Mirai as potential candidates

---

## No "one fits-all approach"

- a combination of tools will probably lead to more results
- static analysis tools combined with provers/model-checkers

---

## Static analysis tools for Rust

- `cargo inspect`
- `mirai` (and other [similar tools](https://github.com/endorlabs/MIRAI/blob/main/documentation/Overview.md))
- taint analysis tools: `polonius`,

---

## Rust verification tools

- Besides RefinedRust, Aenaes, Prusti, maybe worth looking into:
- [Rust foundation initiative to verify standard libs](https://rustfoundation.org/media/rust-foundation-collaborates-with-aws-initiative-to-verify-rust-standard-libraries/) and the [tools they use](https://model-checking.github.io/verify-rust-std/tools.html)
- [Rust verify workshop](https://sites.google.com/view/rustverify2025)

---