Initial formal verification results #69

lgaeher · 2024-07-12T14:00:59Z

Description of the changes

This MR adds our initial verification results.

Type of change

Bug fix (non-breaking change which fixes an issue)
New feature (non-breaking change which adds functionality)
Formal verification
Breaking change (fix or feature that would cause existing functionality to not work as expected)
Refactorization (non-breaking change which improves code quality)

How to test this PR?

Follow the instructions in verification/setup.md to set the formal verification up.
Alternatively, the verify pipeline in CI tests the verification results.

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

Signed-off-by: Wojciech Ozga <woz@zurich.ibm.com>

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

lgaeher · 2024-07-12T14:02:38Z

I still want to make a pass over the annotations and add a bit more documentation before merging it.
But the verification/README.md is ready for review.

wojciechozga

I left a few comments proposing minor changes. I think you are trying to bring the old version of page_allocator which can be simply deleted.

verification/readme.md

wojciechozga · 2024-07-15T11:46:15Z

security-monitor/src/core/memory_layout/mod.rs

@@ -117,6 +181,7 @@ impl MemoryLayout {
    ///
    /// Caller must guarantee that there is no other thread that can write to confidential memory during execution of
    /// this function.
+    // TODO: we need to come up with a mechanism to acquire ownership of all memory


this function is called only when the security monitor is terminating, e.g., due to panic. So the procedure is to first stop all other harts and then execute this function. Since there are no other harts running, we have the ownership of whole confidential memory. I do not know how to express it for the spec purposes, though.

Yeah, expressing this protocol in specification will be difficult -- but it is also not something we need to currently do, since we currently anyways want to prove that there are no panics, so this handler should not be called.

wojciechozga · 2024-07-15T12:02:26Z

security-monitor/src/core/page_allocator/allocator.rs

        let mut smaller_pages = self.page_token.take().unwrap().divide();
        assert!(smaller_pages.len() == self.children.len());
        smaller_pages.drain(..).for_each(|smaller_page_token| {
            let index = self.calculate_child_index(this_node_base_address, this_node_page_size, &smaller_page_token);
            self.children[index].store_page_token_in_this_node(smaller_page_token);
        });
+        let smaller_size = self.max_allocable_page_size.unwrap().smaller().unwrap();
+        self.max_allocable_page_size = Some(smaller_size);


well spotted!
I think it was still working fine because the max_allocable_page_size was then recalculated again based on children's largest available page_size. But, with your fix we satisfy the spec.

wojciechozga · 2024-07-15T12:07:47Z

security-monitor/src/core/page_allocator/allocator.rs

    pub fn acquire_page_token(
        &mut self, this_node_base_address: usize, this_node_page_size: PageSize, page_size_to_acquire: PageSize,
    ) -> Result<Page<UnAllocated>, Error> {
-        assert!(self.max_allocable_page_size >= Some(page_size_to_acquire));
+        //assert!(self.max_allocable_page_size >= Some(page_size_to_acquire));
+        ensure!(self.max_allocable_page_size >= Some(page_size_to_acquire), Error::OutOfPages())?;


well spotted!

looks like it was actually a bug and when we would try to allocate a page that is not available, this code would panic. Something to keep for the paper to say that using formal methods helps to spot these kinds of bugs

wojciechozga · 2024-07-15T12:11:23Z

security-monitor/src/core/page_allocator/page.rs

+    #[rr::args(#raw "#(-[#l; #sz; #tt])")]
+    #[rr::returns("l +ₗ page_size_in_bytes_Z sz")]
+    pub fn end_address_ptr(&self) -> *const usize {
+        // TODO: ideally, use strict-provenance API


Do you mean?

#![feature(strict_provenance)] #![warn(fuzzy_provenance_casts)]

We should indeed use it

Yeah, exactly. We should ideally use pointer::addr() to convert pointers to integers (instead of as usize), and pointer::with_addr() to convert integers to pointers within a known allocation. This will make reasoning quite a bit easier.

This is not something we need to fix now, but I could make a follow-up MR that adapts the code for that.

Sounds good to me. We can add it with another MR.

security-monitor/src/core/page_allocator/page_allocator.rs

Co-authored-by: Wojciech Ozga <woz@zurich.ibm.com> Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

wojciechozga

Thank you for all the changes. It looks good to me!

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

wojciechozga

LGTM

lgaeher · 2024-07-18T18:49:09Z

Thanks for reviewing! As far as I’m concerned, this should be ready for merging, but maybe @shinnar and @gdhh can take a look at the README first.

shinnar

I am not thrilled with current path names: verification/generated_code/ace/proofs/, because it is under generated_code does not look like a manually curated / checked in object. However, I don't have any better suggestions at the moment :-). Anyway, the README.md clearly explains things, and I do not think bikeshedding the path name should hold up this PR.

lgaeher · 2024-07-19T07:15:15Z

Thanks for reviewing! I agree that the path name is not ideal. We could change it to rust_proofs, I think that might capture the content better. What do you think?

security-monitor/src/core/memory_layout/mod.rs

shinnar · 2024-07-19T11:46:05Z

Thanks for reviewing! I agree that the path name is not ideal. We could change it to rust_proofs, I think that might capture the content better. What do you think?

I agree that would be a better name. Also, do we need the ace/ subfolder?

security-monitor/src/core/page_allocator/page.rs

verification/readme.md

gdhh · 2024-07-19T12:34:48Z

verification/readme.md

+## Architecture
+We annotate the Rust source code of the security monitor with verification annotations.
+These include invariants as well as pre- and postconditions.
+


In general the person needs to change.

What do you mean? Would you like one of The user annotates... or The Rust sourcecode is annotated... (passive voice) better? Or do you have something else in mind?

verification/readme.md

gdhh · 2024-07-19T12:36:09Z

verification/readme.md

+This is initiated by running `make verify` in the root directory of the repository.
+
+The generated Coq code is placed in the [`verification/generated_code/ace`](/verification/generated_code/ace) folder.
+It is split into two subfolders, [`generated`](/verification/generated_code/ace/generated) and [`proofs`](/verification/generated_code/ace/proofs).


There are two subfolders,

if this was intended as a reply to my comment above:
yes, generated and proofs. I was referring to ace. concretely, I am proposing
rust_proofs/generated and rust_proofs/proofs (or maybe even rust_proofs/generated and rust_proofs/src?)

I think proofs is a bit clearer than src

gdhh · 2024-07-19T12:47:44Z

verification/readme.md

+The [`generated`](/verification/generated_code/ace/generated) subfolder contains the automatically generated model of the Rust code, the translated specifications, and proof templates.
+It is re-generated on every run of `make verify` and thus should not be modified manually.
+The [`proofs`](/verification/generated_code/ace/proofs) subfolder contains the proofs for the individual functions.
+These files may be modified, as they are not touched by RefinedRust after their initial creation, and may contain partially manual proofs.


These files can be modified because they are not touched by RefinedRust after their initial creation. If the proof is not complete (correct) manual proof steps will need to be added to complete the proof of the function.

The phrase about manual proofs is correct, but manual proofs would not be generated by refined rust.

I am not sure about what you mean by "after their initial creation". For example, if someone goes in a modified the Rust code eventually should that cause everything to be regenerated? All of our annotations are manual right now, so if the rust code is modified does someone has to add/inspect/the annotations? This may be one of the areas where we would like to add some automation ...

I'll change the text to your suggestion, that's a good point.

If someone modifies the Rust code and this breaks the proofs, then someone will have to fix the proofs. This may be because the annotations are now wrong/ the specification is wrong.
The intended workflow is that you change the code, and if everything continues to work, you don't have to inspect anything. Only if something breaks, you know that some work is needed to get the proofs working again.
(Of course, if you change the Rust code by adding new functions, you will generally have to write specifications for those.)

Generally, there should not arise a situation where you need to regenerate everything (including the proof files).

gdhh · 2024-07-19T12:53:23Z

verification/readme.md

+- the page token implementation is documented extensively, so you may learn by example.
+
+## Status
+


Question: do you mean some less interesting verified support modules are not in the table or do you mean we are not verifying "less interesting" support modules? Hopefully the former. If so, somewhere we need to list the less interesting modules that have been verified (does not have to be in the readme).

if we want this table to actually be the verification state then everything must be listed or pointed to so that someone can tell how far we are. ... This is an observation not necessarily required for NIST.

The former, these are not in the table.

I think if someone wants to be able to tell precisely how far we are, they can check this by looking at the annotated Rust files. Anything very detailed is likely prone to getting outdated easily or imposing a high maintenance burden. Probably the high-level modules are something that people will be interested in, but not which auxiliary functions precisely are verified.

But maybe we can discuss this more offline, if it's not required for this MR?

I agree that we cannot keep the README to detailed because we will most likely get out of sync with the source code. So a high level concepts should be enough at this stage. Once the verification is complete we might think to be more specific because the frequency of changes will be much smaller. All in all, I would keep it like it is now. We can discuss during our Mondays sync meetings.

verification/readme.md

lgaeher · 2024-07-19T16:05:42Z

I agree that would be a better name. Also, do we need the ace/ subfolder?

I guess the ace subfolder could be renamed, maybe to security_monitor. It is there because there are other crates with utility functions, like the pointer utility crate, which we should also verify. Then we would have more subfolders, one for each crate.

shinnar · 2024-07-19T16:10:52Z

yes, I think that renaming to security_monitor makes sense. So the path schema would be

rust_proofs/CRATE_NAME/generated
rust_proofs/CRATE_NAME/proofs

lgaeher · 2024-07-19T16:37:20Z

yes, I think that renaming to security_monitor makes sense. So the path schema would be

Actually, it's currently called ace not because of a RefinedRust-specific naming scheme, but because the Rust crate is called ace in security-monitor/Cargo.toml. Renaming it would also affect how clients can link to it, but not sure if it is used that way by anyone currently. @wojciechozga do you think it's a good idea to rename the crate, or would you prefer to keep it at ace?

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

wojciechozga

I made a pass over the changes after all comments and it looks ready to be merged. We can change the crate name in future PR. @lgaeher thank you for this contribution!

lgaeher and others added 11 commits July 10, 2024 13:34

Work on Page verification

e36bd02

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

work on spec for page allocator

028125f

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

simplifying page table memory representation

014bcd2

Signed-off-by: Wojciech Ozga <woz@zurich.ibm.com>

more work on page

f3a117c

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

work on new page allocator spec

3498f9d

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

add readme document outlining the verification

31a38a2

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

build fixes

159276c

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

fix build

93b2363

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

bump opensbi

c8af232

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

fix build script

23e671e

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

ci fixes

fb3c99e

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

lgaeher marked this pull request as draft July 12, 2024 14:01

lgaeher requested a review from wojciechozga July 12, 2024 14:02

wojciechozga assigned gdhh and shinnar Jul 12, 2024

wojciechozga requested changes Jul 15, 2024

View reviewed changes

lgaeher and others added 3 commits July 16, 2024 15:29

Include suggestions in readme

67352a2

Co-authored-by: Wojciech Ozga <woz@zurich.ibm.com> Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

change makefile message

b5692de

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

work on cleanups

4735e62

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

wojciechozga approved these changes Jul 17, 2024

View reviewed changes

lgaeher added 2 commits July 17, 2024 12:38

some coq refactoring

3c68342

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

clean up page table

8ce19f4

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

lgaeher force-pushed the ci/lennard/verification branch from 616fb6f to 8ce19f4 Compare July 17, 2024 18:02

lgaeher marked this pull request as ready for review July 18, 2024 07:46

lgaeher changed the title ~~Draft: initial formal verification results~~ Initial formal verification results Jul 18, 2024

wojciechozga approved these changes Jul 18, 2024

View reviewed changes

shinnar approved these changes Jul 18, 2024

View reviewed changes