Authenticated Firmware Loaders: Verification and Potential Vulnerabilities

This research paper explores the verification of authenticated firmware loaders presented by Sujit Kumar Muduli, Pramod Subramanyan, and Sayak Ray. It delves into the secure boot process to prevent malicious firmware compromise. The study also discusses trusted firmware updates for remote device security, along with examples of protocols and potential vulnerabilities like state hijacking, TOCTOU, and confused deputy attacks.

• Firmware Loaders
• Verification
• Security
• Remote Devices
• Potential Vulnerabilities

bre_ha Follow

Uploaded on Oct 11, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Verification of Authenticated Firmware Loaders Sujit Kumar Muduli1, Pramod Subramanyan1, Sayak Ray2 Indian Institute of Technology, Kanpur1 Intel Corporation, Hillsboro, OR2 FMCAD-2019, San Jose (Research funded in part by the Semiconductor Research Corporation) 1

2. Introduction Authenticated Firmware Loaders Secure boot process booting malicious firmware can compromise whole system Valid image malicious image secure boot process Trusted firmware update authenticates firmware updates on remote devices updating remote device firmware 2

3. Example Protocol 3

4. Example Protocol (SoC Platform) Boot Image ??1 ??2 Flash AES MMU SHA256 RSA ROM N/W trusted un-trusted RAM 4

5. Example Protocol (Image Format) image header contains hash of each data block signature for header integrity data block base: memory address for a data block size: size of the data block data: payload to be stored 5

6. Example Protocol start loadHeader check header invalidHeader loadBlock reloc block gotoVerifyBlock loadNextBlock invalidBlock verify block abort !(hasNextBlock) success 6

7. What are Potential Vulnerabilities? 1. State hijacking attack 2. TOCTOU attack 3. Confused deputy attack 7

8. State Hijacking Attack 8

9. State Hijacking Attack start ?????? ?????? ?????0 ?????1 ?????2 ... ?????? 1 ??1 ??1 ?????0 ??2 ??2 Flash loadHeader check header invalidHeader loadBlock reloc block invalid image in Flash Storage AES gotoVerifyBlock MMU loadNextBlock SHA256 invalidBlock verify block RSA abort !(hasNextBlock) ROM Protocol state variable location N/W success RAM 9

10. TOCTOU Attack (Time of Check to Time of Use) 10

11. TOCTOU Attack (Time of Check to Time of Use) start ?????? ?????0 ?????1 ?????2 ... ?????? 1 ?????? ??1 ??1 ??2 ??2 ?????0 ?????1 Flash loadHeader check header invalidHeader loadBlock reloc block AES gotoVerifyBlock MMU loadNextBlock SHA256 invalidBlock verify block RSA abort !(hasNextBlock) ROM N/W success RAM 11

12. TOCTOU Attack (Time of Check to Time of Use) RAM Preventing TOCTOU attack mark image locations in RAM as READ_ONLY for others accelerators: READ/WRITE permission to protocol firmware still vulnerable to Confused Deputy attack attacker: READ_ONLY permission to others 12

13. Confused Deputy Attack 13

14. Confused Deputy Attack start ?????? ?????0 ?????1 ?????2 ... ?????? 1 ??1 ??2 ??2 Flash loadHeader check header invalidHeader loadBlock No write permission reloc block AES gotoVerifyBlock MMU loadNextBlock SHA256 invalidBlock verify block RSA Trusted accelerators have R/W permissions ?????? abort !(hasNextBlock) ROM ?????0 ??2 can make them to write data to target location in RAM N/W ?????1 success RAM 14

15. Challenges in Specification 15

16. Challenges in Specification A strawman property specification to capture protocol security authentication succeeds if and only if Image binary has valid header and each block has a valid hash tamper data block tamper header loads malicious firmware starts with valid image {load header} {success} {check header} {start} {verify block} {reloc block} implementation satisfying the property could still be vulnerable to TOCTOU and confused deputy attacks 16

17. System Model 17

18. System Model (w/o Adversary Model) Property : if image is authenticated successfully, then it is a valid image. start loadHeader ??+1 ?0 ?? ?1 check header invalidHeader loadBlock reloc block (trace for valid image) gotoVerifyBlock loadNextBlock invalidBlock verify block abort !(hasNextBlock) (trace for invalid image) success 18

19. System Model + Adversary Model Boot Loader in adversarial setting ????= ?????????? ??????????????? start loadHeader check header ?? ???? invalidHeader loadBlock reloc block gotoVerifyBlock loadNextBlock invalidBlock verify block ?? ???? abort !(hasNextBlock) Tamper relation (tmpr) : captures adversary actions arbitrary memory write operations (image tampering) RowHammer attack (model using bitflips) actions of untrusted software components success Boot Loader 19

20. System Model Verifying Boot Loader in adversarial setting accept ?1 ??????(????) same boot image accept ?2 ??????(?) For all ?? ?????? ???? there exists corresponding ?? ?????? ? s.t. ?????? ?? ??????(??) ???? ?? ????(??) Quantifier Alternation (presence of both and difficult to verify) 20

21. System Model Addressing quantifier alternation issue Construct an overapproximate model (????+) Adversary actions : {tmpr, NOP} ? and ???? refines ????+ 21

22. System Model Addressing quantifier alternation issue Decompose security property into easier to verify 2-safety properties 1) No Hijacking Property 2) No TOCTOU Property 22

23. Verifying Overapproximated Model 2-Safety Property to verify : No state hijacking accept tmpr tmpr tx ?1 same boot image NOP NOP tx ?2 ?0 ?0 accept ?????? ?? ??????(??) Counterexample Trace accept tmpr tx ?1 abort tx NOP NOP ?2 ?0 ?0 23

24. Verifying Overapproximated Model 2-Safety Property to verify : No TOCTOU accept tx ?1 same boot image ???? ???? ???? ???? ?2 ?0 ?0 tx NOP NOP accept Image data doesn t get tampered by adversary 24

25. Verifying Overapproximated Model 2-Safety Property to verify : No TOCTOU accept tx ?1 ???? ???? ???? ???? NOP NOP tx ?2 ?0 ?0 accept Counter Example Trace accept tmpr tx ?1 ???? ?? ????(??) ???? ???? NOP NOP tx ?2 ?0 ?0 accept 25

26. Verifying Overapproximated Model ????and ? refines ????+ ????+ satisfies ?? ????? ????????? and ?? ?????? ???? and ? satisfies the security property 26

27. Non-Interference for Security Protocols Noninterference properties describes strong security requirements E.g. regardless of what the adversary s actions are, the system must boot a valid image accept tx ?1 NOP NOP tx ?2 ?0 ?0 accept ?????? ?? ??????(??) 27

28. Results The protocol, adversary actions and properties are modeled using UCLID5 Bit Width No state hijack property No TOCTOU property Standard safety property verified compositionally (a) (b) (c) 8 4.3s 5.2s 8.2s 3.0s 2.8s 12 4.9s 12.9s 12.1s 3.0s 2.7s 16 4.6s 15.0s 9.0s 3.4s 2.9s 24 6.4s 13.8s 26.2s 3.4s 3.2s 32 7.8s 16.5s 18.5s 4.3s 3.2s 28

29. code https://bitbucket.org/spramod/verif-auth-loader/src/master/ 29