Cargocallstack Static Callstack Analysis for Rust Memory safety is instrumental to the safety and security of software systems. The Rust language stands out with a type system and underlying memory model targeting memory safety without the need for dynamic garbage collection, making Rust a viable option for embedded applications. In this paper we present an integrated tool for callstack analysis of Rust applications. We cover both theoretical and practical challenges, their solutions and open questions. The cargocallstack tool is useful for analyzing Rust applications in general, and embedded Rust in particular. To the latter, we show that using the callstack analysis we can give guarantees of total memory safety, free of assumptions on operating systems and underlying memory protection mechanisms in hardware. The feasibility of the approach is demonstrated by applying the xe2x80x98callstackxe2x80x99 tool on production code targeting a lightweight ARM CortexM platform.

Verification of Safety Functions Implemented in Rust  a Symbolic Execution based approach Symbolic execution allows us to observe and assert properties of program code executing under (partially) unknown inputs and state. In this work we present a case study demonstrating that safety functions implemented in the Rust programming language can be verified by an assertion based approach. To this end, we leverage on previous developments adopting LLVMKLEE for symbolic execution of Rust programs.In particular we show that reliability can be ensured by proven absence of undefined behavior and that safety properties (expressed as assertions) can be ensured for all reachable paths of the underlying implementation (under symbolic inputs). Moreover, the verification (besides stating assertions) is fully automatic and can be applied without any changes made to the implementation. While assertions have the advantage of being familiar to the mainstream programmer, they lack the expressiveness of dedicated logic developed for model checking. The paper also discusses complexity issues arising from pathstate explosion inherent to symbolic execution. The feasibility of the approach is demonstrated on a representative use case implementing a safety function (equality) from the PLCopen library. We obtain complete path (466) and state (8) coverage in under 2 seconds for the given example on an i77700 laptop computer.