[HN Gopher] Formal CHERI: design-time proof of architecture secu...
       ___________________________________________________________________
        
       Formal CHERI: design-time proof of architecture security properties
        
       Author : pabs3
       Score  : 26 points
       Date   : 2022-07-22 06:20 UTC (16 hours ago)
        
 (HTM) web link (www.lightbluetouchpaper.org)
 (TXT) w3m dump (www.lightbluetouchpaper.org)
        
       | gnufx wrote:
       | It's worth checking out Peter Sewell's talks in this area. A
       | classic is https://media.ccc.de/v/31c3_-_6574_-_en_-
       | _saal_1_-_201412301...
        
       | egberts1 wrote:
       | While not an absolute proof of an absolute security model of a
       | concurrent (interrupt-based) CPU as its first primary focus is
       | baby-step ensuring a secured proof using a sequential CPU model
       | (with a few omitted features, I'm guessing a cache of any level
       | amongst others that I couldn't notice), this definitely paved the
       | way toward solid theoretical proofing toward hardware security in
       | general.
       | 
       | With this Herculean task being accomplished, I do see further
       | automated HW security proofing on lesser CPU architecture (FFA,
       | sequential embedded microcontrollers such as motor controller, RF
       | controllers, power level monitor, etc.).
       | 
       | Seems like the next generation of HW security proofing is caching
       | (if not done already), context switching, interrupt, and multi-
       | CPU.
       | 
       | Any error above is mine and mine alone.
       | 
       | We live in interesting time.
        
       ___________________________________________________________________
       (page generated 2022-07-22 23:01 UTC)