Add RAPx tool description and CI workflow

[DiuDiu777]

This PR adds the tool description and workflow for RAPx.

Since we plan to try challenge 23 for verifying Vec, we use the vec::into_raw_parts_with_alloc API as an example in this PR. It demonstrates how to annotate the target function and mark relevant unsafe callees with safety tags for RAPx verification.

Related issue: Add Tool: RAPx

[btj]

Hi @DiuDiu777 ! Very excited to see another participant entering the contest.

I'm trying to understand your approach. In particular, I'm reading the Unsafe Code Audit chapter of the RAPx Book. Could it be that there are some typos in the code examples?

• Function f calls SecretRegion::from(p, 0) but p is of type *mut u32 and from requires a Vec<u32>?
• What's the point of the len field? It's never read?
• In the annotations for offset:
  • Should it be InBound instead of InBounded?
  • Is a precondition saying that isize::MIN <= count * size_of::<T>() missing?
• Annotations for xor_secret_region:
  • Are these automatically generated or manually annotated?
  • self is of type &SecretRegion, right? That struct's fields are buffer, of type Vec<u32>, and len, not buffer, of type *mut u32, and size, as this listing seems to assume?
  • region should be self?

Is there a paper arguing the soundness of your unsafe code audit approach with respect to a formal semantics of the programming language (such as I do in Featherweight VeriFast)? I found this paper but it does not seem to make any soundness claims.

[btj]

Also, your example in the book is still somewhat complex. It would be very helpful, I think, if you could do a similar walkthrough for Vec::into_raw_parts_with_alloc, which seems even simpler. How exactly does your tool verify this function? Many thanks in advance!

[DiuDiu777]

Hi, @btj . Thank you so much for your careful review and thoughtful feedback!

Regarding your questions:

• Function f calls SecretRegion::from(p, 0) but p is of type *mut u32 and from requires a Vec<u32>?
• What's the point of the len field? It's never read?

• The code example is primarily meant to illustrate annotation and verification logic, so some parts may not be fully realistic.

• In the annotations for offset:

• You're right, there are typos in the annotations and we'll correct those.

• Are these automatically generated or manually annotated?

• The xor_secret_region annotations are manually added, similar to how we handle standard library functions to be verified.

• self is of type &SecretRegion, right? That struct's fields are buffer, of type Vec<u32>, and len, not buffer, of type *mut u32, and size, as this listing seems to assume?
• region should be self?

• The struct fields should indeed align with the definition – we'll update the example to use buffer.

As for the soundness and complexity of examples, we're currently refining the document to better explain soundness guarantees and simplify examples where possible. Thanks again for your valuable input!

[hxuhack]

Hi @btj , thanks for reviewing our work. I have written a short article that explains why our core methodology, tracing-based verification, is sound.

[btj]

Hi @hxuhack , many thanks for the article. However, I had hoped that it would clarify the key concepts of your approach, such as unsafety propagation graph, object flow edge, basic unit, audit unit, safety property, dominated graphs, contractual invariant states, operational trace states, vulnerable paths, constructor analysis, and method sequence analysis. It would be very useful to see a formal definition of (simplified versions of) these concepts, and a formal definition of the overall unsafe code audit approach, and then a rigorous proof relating these concepts to a formal syntax and semantics of (a simplified version of) Rust, showing that if the approach accepts the program, then the program has no Undefined Behavior. Something like what we did in the Featherweight VeriFast paper.

Here are some specific questions to which I did not immediately find an answer in the materials currently available:

A. Would your tool detect the error in the following incorrect version of Vec::into_raw_parts_with_alloc? If so, how?

    pub fn into_raw_parts_with_alloc(self) -> (*mut T, usize, usize, A) {
        let mut me = self; // was: let mut me = ManuallyDrop::new(self);
        let len = me.len();
        let capacity = me.capacity();
        let ptr = me.as_mut_ptr();
        let alloc = unsafe { ptr::read(me.allocator()) };
        (ptr, len, capacity, alloc)
    }

B. Would your tool detect the error in the following incorrect version of Vec::into_raw_parts_with_alloc? If so, how?

    pub fn into_raw_parts_with_alloc(self) -> (*mut T, usize, usize, A, A) {
        let mut me = ManuallyDrop::new(self);
        let len = me.len();
        let capacity = me.capacity();
        let ptr = me.as_mut_ptr();
        let alloc = unsafe { ptr::read(me.allocator()) };
        let alloc2 = unsafe { ptr::read(me.allocator()) }; // I added this line
        (ptr, len, capacity, alloc, alloc2)
    }

C. Would your tool detect the error in the following incorrect version of Vec::into_raw_parts_with_alloc? If so, how?

    pub fn into_raw_parts_with_alloc(self) -> (*mut T, usize, usize, A) {
        let mut me = Box::new(self);
        let len = me.len();
        let capacity = me.capacity();
        let ptr = me.as_mut_ptr();
        let allocator_ptr = me.allocator() as *const A;
        drop(me);
        let alloc = unsafe { ptr::read(allocator_ptr) };
        (ptr, len, capacity, alloc)
    }