How will verifications hold up over time? And how can the verifications themselves be trusted?

[Mike4Online]

If a given standard/core library function uses unsafe calls, and someone verifies that the unsafe code is safe and proper in practice, how will that verification hold up over time? I.E. the verification represents an approval of the code at a specific point in time. If library maintainers want to alter a standard library method that (1) has an unsafe section, and (2) has been verified safe in practice, then their modifications to the unsafe portion of the method could (should?) invalidate the prior verification.

One possibility is code comments that would mark the beginning and ending of a range of code that has been verified. The comments could include a hash of the code lines which appear between these opening and closing comments, so that if a maintainer alters any code in the future between these comments, the hash would change and thus invalidate the verification (i.e. require a re-verification and an update to the verification comments and hash). This would need to be supported by a tool to make it easy to mark sections of code and calculate the hash value.

Taking a step back, the nature of the verification may be suspect. Did a given verification cover memory management, race conditions, bounds checking, undefined behavior, and any number of other potential issues? I.E. was the verification comprehensive? And was the verification done in a manner that was proper, i.e. can the verification be trusted to have been done well? What safeguard is there if someone verifies that a given unsafe function is safe in practice, but they botched the verification and missed a subtle issue or edge case?

I'm not trying to knock this effort. But it seems like a band-aid over a larger issue of how can we be assured that our code behaves within the bounds of sanctioned behaviors, i.e. is "safe".

[patricklam]

Hi Michael, The idea with push-button verification is that it is easy to re-run when the verified code has been changed. Indeed, this effort comes with CI scripts that should automatically run the verification when either the verification scripts (proof harnesses) change, or the code itself changes. The meaning of Rust "unsafe" is somewhat surprising. In standard Rust, it means that there are some safety properties that the caller is supposed to ensure. If these properties hold, then the unsafe code should not do anything bad. (You can find more about this in section 2 of our HATRA paper: https://patricklam.ca/papers/24.hatra.rust-verification.pdf). For this effort, exactly what is verified comes down to the preconditions and postconditions that actually get verified, modulo the soundness of the tool. I believe that Kani is designed to be sound. In particular, it exhaustively checks up to a given scope and should raise a verification error if this is insufficient. (We discussed that near the end of Section 3 of the HATRA paper). pat

…

On Sat, Nov 23, 2024 at 7:26 PM Michael Litwak ***@***.***> wrote: If a given standard/core library function uses unsafe calls, and someone verifies that the unsafe code is safe and proper in practice, how will that verification hold up over time? I.E. the verification represents an approval of the code at a specific point in time. If library maintainers want to alter a standard library method that (1) has an unsafe section, and (2) has been verified safe in practice, then their modifications to the unsafe portion of the method could (should?) invalidate the prior verification. One possibility is code comments that would mark the beginning and ending of a range of code that has been verified. The comments could include a hash of the code lines which appear between these opening and closing comments, so that if a maintainer alters any code in the future between these comments, the hash would change and thus invalidate the verification (i.e. require a re-verification and an update to the verification comments and hash). This would need to be supported by a tool to make it easy to mark sections of code and calculate the hash value. Taking a step back, the nature of the verification may be suspect. Did a given verification cover memory management, race conditions, bounds checking, undefined behavior, and any number of other potential issues? I.E. was the verification comprehensive? And was the verification done in a manner that was proper, i.e. can the verification be trusted to have been done well? What safeguard is there if someone verifies that a given unsafe function is safe in practice, but they botched the verification and missed a subtle issue or edge case? I'm not trying to knock this effort. But it seems like a band-aid over a larger issue of how can we be assured that our code behaves within the bounds of sanctioned behaviors, i.e. is "safe". — Reply to this email directly, view it on GitHub <#182>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAOKE5QN72W6FYRNIXLFAB32CANXZAVCNFSM6AAAAABSKXUFFOVHI2DSMVQWIX3LMV43ERDJONRXK43TNFXW4OZXGUZTOMRTGU> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[celinval]

@Mike4Online, those are great questions.

First, as @patricklam pointed out, we have been focusing on automatic verification and CI integration due to similar concern. We don't want the verification to become obsolete. We also periodically update this repository with newer versions of the Rust standard library.

Second, I believe this effort is a step in the right direction. Each verification tool will have its strengths and weaknesses, so people should be aware of them, but they are constantly evolving, the same way the Rust language is. Our goal is to push the boundaries of verification so it can provide meaningful safety guarantees for the Rust standard library.