Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Global ASM is not supported #316

Open
1 of 3 tasks
danielsn opened this issue Jul 8, 2021 · 2 comments
Open
1 of 3 tasks

Global ASM is not supported #316

danielsn opened this issue Jul 8, 2021 · 2 comments
Assignees
@zhassan-aws
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct
Milestone
Soundness

Comments

@danielsn
Copy link
Contributor

danielsn commented Jul 8, 2021 •
edited
Loading

Following LLVM, Rust allows global ASM in a module. This means that crates can have arbitrary code that we cannot analyze.

Likelihood

We know of crates that use this feature

Mitigation

We could fail any crate that uses this feature, but this would block any use of those crates, even if they did not use any of the risky features. Even worse, this would block all consumers of such crates, from even compiling, again even if they do not use any of the dangerous features.

Unlike for inline ASM in a function, where we can insert assert(0) as a mechanism to guarantee soundness, there is no obvious way to only fail code paths that use the injected ASM.

  • Raise a warning if global asm appears
  • Incorporate that warning into viewer

Path to soundness

  • Support ASM in CBMC

Documentation

https://rust-lang.github.io/rfcs/1548-global-asm.html
@danielsn danielsn added this to the Soundness milestone Jul 8, 2021
@adpaco-aws
Copy link
Contributor

adpaco-aws commented Jul 19, 2021 •
edited
Loading

The "Raise a warning" item can be marked as done, right?

@zhassan-aws zhassan-aws mentioned this issue Oct 29, 2021
Open
@danielsn danielsn modified the milestones: Soundness, RMC MLP Dec 8, 2021
@zhassan-aws zhassan-aws self-assigned this Apr 19, 2022
@zhassan-aws
Copy link
Contributor

Capturing the current behavior as of c3d41b9: Kani produces a codegen warning, but does not cause verification to fail. For example, on the following test (adapted from the one here):

pub mod sally {
    std::arch::global_asm!(
        ".global foo",
        "foo:",
        "jmp baz",
    );

    #[no_mangle]
    pub unsafe extern "C" fn baz() {}
}

// the symbols `foo` and `bar` are global, no matter where
// `global_asm!` was used.
extern "C" {
    fn foo();
    fn bar();
}

pub mod harry {
    std::arch::global_asm!(
        ".global bar",
        "bar:",
        "jmp quux",
    );

    #[no_mangle]
    pub unsafe extern "C" fn quux() {}
}

#[kani::proof]
fn main() {
    assert!(1 + 1 == 2);
}

Kani produces two codegen warnings:

 WARN kani_compiler::codegen_cprover_gotoc::compiler_interface Crate global_asm contains global ASM, which is not handled by Kani
 WARN kani_compiler::codegen_cprover_gotoc::compiler_interface Crate global_asm contains global ASM, which is not handled by Kani
warning: 2 warnings emitted

but verification passes:

RESULTS:
Check 1: main.assertion.1
         - Status: SUCCESS
         - Description: "assertion failed: 1 + 1 == 2"
         - Location: global_asm.rs:32:5 in function main


SUMMARY: 
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL

@celinval celinval added [F] Soundness Kani failed to detect an issue and removed Soundness: High labels Apr 20, 2022
@zhassan-aws zhassan-aws mentioned this issue Apr 20, 2022
Closed
4 tasks
@zhassan-aws zhassan-aws mentioned this issue Apr 26, 2022
Merged
4 tasks
@celinval celinval added [C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. and removed [F] Soundness Kani failed to detect an issue T-Mitigated labels Nov 9, 2022
@celinval celinval changed the title Soundness: Global ASM Global ASM is not supported Nov 9, 2022
@celinval celinval added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct and removed [C] Bug This is a bug. Something isn't working. [F] Spurious Failure Issues that cause Kani verification to fail despite the code being correct. labels Nov 9, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@zhassan-aws zhassan-aws

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. [E] Unsupported Construct Add support to an unsupported construct
Projects
None yet
Milestone
Soundness
Development

No branches or pull requests
4 participants
@danielsn @celinval @adpaco-aws @zhassan-aws