4 ms·

The key results: > Cascade discovered 12 bugs that produce wrong computations under certain microarchitectural conditions (Uarchvals) in Kronos and VexRiscv >

The key results: > Cascade discovered 12 bugs that produce wrong computations under certain microarchitectural conditions (Uarchvals) in Kronos and VexRiscv > Cascade discovered 3 bugs that cause hangs in Kro- nos, PicoRV32 and VexRiscv These are the hard bugs to find in the implementation of the CPU > Cascade discovered 4 bugs in BOOM and CVA6 that produce wrong output val- ues regardless of the microarchitectural state These are unacceptable bugs, showing a lack of architectural tests. It means no one ever ran those instructions and checked the result. The community should be able to fix this.

deleted 3y ago
[deleted]
rowanG077 3y ago
> It means no one ever ran those instructions and checked the result. That's not really true. It means they produced wrong values with some input. They may have tested but not hit the pathological input case. No one is going to sweep the entirety of the domain. You really need a formal proof to avoid these bugs.
- flaviens 3y ago
  Correct. One beneficial thing with Cascade's long programs with dependencies is that it will tendentially produce problematic values (values around NaNs, around zero, etc.). Formal methods won't be replaced by Cascade :) but it's another amount of work
- nickpsecurity 3y ago
  If doing the formal route, then Centaur's reports are worth looking at for using ACL2: https://www.researchgate.net/publication/267809758_Use_of_Formal_Verification_at_Centaur_Technology https://www.researchgate.net/publication/267809758_Use_of_Fo... https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.pdf https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.p... (Note: That one is kind of a marketing piece, too.) In high-assurance systems, both formal methods and exhaustive testing are supposed to be used. I'd be curious to see the results of the submitted tech on designs such as the VAMP processor and Rockwell Collins AAMP7G. https://www.researchgate.net/publication/220643416_Putting_it_all_together_-_Formal_Verification_of_the_VAMP https://www.researchgate.net/publication/220643416_Putting_i... https://www.khoury.northeastern.edu/home/pete/acl206/slides/hardin.pdf https://www.khoury.northeastern.edu/home/pete/acl206/slides/...
  - rowanG077 3y ago
    Exhaustive testing is used? Only in some very special cases that can be done... Take the PMULLD instruction. It takes two 128-bit inputs. If you assume you can verify one input in 1ns. An exhaustive test will take 3.67 × 10^60 years. Orders of magnitude longer then the age of the universe.
    - nickpsecurity 3y ago
      I meant it figuratively. Safety and security certification at high levels often required that every module and function be tested. That was on top of black box testing and pen testing. Some practitioners added fuzz testing, path-based, symbolic, combinatorial, etc. So, not literally exhaustive. They just covered every function, feature, interface, and combination that might trigger a bug. Although, some rare folks did do literally- exhaustive testing of algorithms and FSM’s on 8-bit MCU’s since they had 256 values per variable. Others and I put timers on loops to force it to be terminating and just analyzed those cases. One could use exhaustive testing in the small to justify modeling a function with a specific formula. If you have several of those, then methods like Cleanroom Software Engineering let you semiformally verify the correctness of upper layers. So, there’s some stuff like that which was used on an ad hoc basis. Most just tested values and combinations likely to trigger bugs since they were in ranges that cause effects.
_chris_ 3y ago
> > Cascade discovered 4 bugs in BOOM and CVA6 that produce wrong output val- ues regardless of the microarchitectural state > These are unacceptable bugs, showing a lack of architectural tests. It means no one ever ran those instructions and checked the result. The community should be able to fix this. For BOOM it looks like the only 2 bugs found were miscounting on the inst-retired perf counter if software over-wrote it, and a fdiv.s/fsqrt.s that always listened to the dynamic rounding mode instead of the statically provided rounding mode, when specified. Not great, but recoverable.

deleted 3y ago

[deleted]

rowanG077 3y ago

> It means no one ever ran those instructions and checked the result. That's not really true. It means they produced wrong values with some input. They may have tested but not hit the pathological input case. No one is going to sweep the entirety of the domain. You really need a formal proof to avoid these bugs.

flaviens 3y ago
Correct. One beneficial thing with Cascade's long programs with dependencies is that it will tendentially produce problematic values (values around NaNs, around zero, etc.). Formal methods won't be replaced by Cascade :) but it's another amount of work
nickpsecurity 3y ago
If doing the formal route, then Centaur's reports are worth looking at for using ACL2: https://www.researchgate.net/publication/267809758_Use_of_Formal_Verification_at_Centaur_Technology https://www.researchgate.net/publication/267809758_Use_of_Fo... https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.pdf https://www.cs.utexas.edu/users/hunt/talks/2021-11-Centaur.p... (Note: That one is kind of a marketing piece, too.) In high-assurance systems, both formal methods and exhaustive testing are supposed to be used. I'd be curious to see the results of the submitted tech on designs such as the VAMP processor and Rockwell Collins AAMP7G. https://www.researchgate.net/publication/220643416_Putting_it_all_together_-_Formal_Verification_of_the_VAMP https://www.researchgate.net/publication/220643416_Putting_i... https://www.khoury.northeastern.edu/home/pete/acl206/slides/hardin.pdf https://www.khoury.northeastern.edu/home/pete/acl206/slides/...
- rowanG077 3y ago
  Exhaustive testing is used? Only in some very special cases that can be done... Take the PMULLD instruction. It takes two 128-bit inputs. If you assume you can verify one input in 1ns. An exhaustive test will take 3.67 × 10^60 years. Orders of magnitude longer then the age of the universe.
  - nickpsecurity 3y ago
    I meant it figuratively. Safety and security certification at high levels often required that every module and function be tested. That was on top of black box testing and pen testing. Some practitioners added fuzz testing, path-based, symbolic, combinatorial, etc. So, not literally exhaustive. They just covered every function, feature, interface, and combination that might trigger a bug. Although, some rare folks did do literally- exhaustive testing of algorithms and FSM’s on 8-bit MCU’s since they had 256 values per variable. Others and I put timers on loops to force it to be terminating and just analyzed those cases. One could use exhaustive testing in the small to justify modeling a function with a specific formula. If you have several of those, then methods like Cleanroom Software Engineering let you semiformally verify the correctness of upper layers. So, there’s some stuff like that which was used on an ad hoc basis. Most just tested values and combinations likely to trigger bugs since they were in ranges that cause effects.

_chris_ 3y ago

> > Cascade discovered 4 bugs in BOOM and CVA6 that produce wrong output val- ues regardless of the microarchitectural state > These are unacceptable bugs, showing a lack of architectural tests. It means no one ever ran those instructions and checked the result. The community should be able to fix this. For BOOM it looks like the only 2 bugs found were miscounting on the inst-retired perf counter if software over-wrote it, and a fdiv.s/fsqrt.s that always listened to the dynamic rounding mode instead of the statically provided rounding mode, when specified. Not great, but recoverable.