Skip to main content

Undermining Isolation Through Covert Channels in the Fiasco.OC Microkernel

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Electrical Engineering ((LNEE,volume 363))

Abstract

System designers have come to recognize the merits of building critical systems on top of small kernels for their ability to provide strong isolation at system level. This is due to the fact that enforceable isolation is the prerequisite for any reasonable security policy. Towards this goal we examine some internals of Fiasco.OC, a microkernel of the prominent L4 family. Despite its recent success in certain high-security projects for governmental use, we prove that Fiasco.OC is not suited to ensure strict isolation between components meant to be separated. Unfortunately, in addition to the construction of system-wide denial of service attacks, our identified weaknesses of Fiasco.OC also allow covert channels across security perimeters with high bandwidth. We verified our results in a strong affirmative way through many practical experiments. Indeed, for all potential use cases of Fiasco.OC we implemented a full-fledged system on its respective archetypical hardware: Desktop server/workstation on AMD64 x86 CPU, Tablet on Intel Atom CPU, Smartphone on ARM Cortex A9 CPU. The measured peak channel capacities ranging from \(\sim \)13,500 bits/s (Cortex-A9 device) to \(\sim \)30,500 bits/s (desktop system) clearly falsify Fiasco.OC’s isolation guarantee.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Quota objects can be shared among multiple tasks.

  2. 2.

    mapping database.

  3. 3.

    Since a page address is always aligned to the page size, the lower bits of the mapping address can be used for the depth in the mapping tree.

  4. 4.

    Unlike regular voice calls, VoIP calls are not handled by the baseband processor but by the application processor.

References

  1. Apt1: Exposing one of China’s cyber espionage units (2013)

    Google Scholar 

  2. Apt28: A window into russia’s cyber espionage operations? (2014)

    Google Scholar 

  3. Bishop, M.A.: Computer Security. Addison-Wesley Professional, Art and Science (2002)

    Google Scholar 

  4. Clarke, R., Knake, R.: Cyber War: The Next Threat to National Security and What to Do About It. Ecco (2012)

    Google Scholar 

  5. Fiasco.oc website (2014). http://os.inf.tu-dresden.de/fiasco/

  6. Genua cyber-top. https://www.genua.de/loesungen/security-laptop-cyber-top.html

  7. Karger, P., Zurko, M., Bonin, D., Mason, A., Kahn, C.: A vmm security kernel for the vax architecture. In: Proceedings of the IEEE Computer Society Symposium on Research in Security and Privacy, 2–19 (1990)

    Google Scholar 

  8. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: Sel4: formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP ’09, 207–220, New York, USA (2009). (ACM)

    Google Scholar 

  9. L4re-based simko 3 security smartphone wins bsi approval for classified data (2013). http://www.kernkonzept.com

  10. Liedtke, J.: Improving ipc by kernel design. SIGOPS Oper. Syst. Rev. 27(5), 175–188 (1993)

    Article  Google Scholar 

  11. Liedtke, J.: On micro-kernel construction. SIGOPS Oper. Syst. Rev. 29(5), 237–250 (1995)

    Article  Google Scholar 

  12. Lin, Y., Ding, L., Wu, J., Xie, Y., Wang, Y.: Robust and efficient covert channel communications in operating systems: design, implementation and evaluation. In: Proceedings of the IEEE 7th International Conference on Software Security and Reliability-Companion (SERE-C), 45–52 (2013)

    Google Scholar 

  13. Lipinski, B., Mazurczyk, W., Szczypiorski, K.: Improving hard disk contention-based covert channel in cloud computing environment. arXiv preprint (2014). arXiv:1402.0239

  14. Okamura, K., Oyama, Y.: Load-based covert channels between xen virtual machines. In: Proceedings of the 2010 ACM Symposium on Applied Computing, SAC ’10, 173–180, New York, USA (2010). (ACM)

    Google Scholar 

  15. Ristenpart, T., Tromer, E., Shacham, H., Savage, S.: Hey, you, get off of my cloud: exploring information leakage in third-party compute clouds. In: Proceedings of the 16th ACM Conference on Computer and Communications Security, CCS ’09, 199–212, New York, USA (2009). (ACM)

    Google Scholar 

  16. Simko–sichere mobile kommunikation (2014). http://security.t-systems.de/loesungen/mobile-simko

  17. Suzaki, K., Iijima, K., Yagi, T., Artho, C.: Memory deduplication as a threat to the guest os. In: Proceedings of the Fourth European Workshop on System Security, EUROSEC ’11, 1:1–1:6, New York, USA (2011). (ACM)

    Google Scholar 

  18. Technical features - Minnowboard (2014). http://www.minnowboard.org/technical-features/

  19. Technical features–Pandaboard (2014). http://pandaboard.org/content/platform

  20. Wu, J., Ding, L., Lin, Y., Min-Allah, N., Wang, Y.: Xenpump: a new method to mitigate timing channel in cloud computing. In: Proceedings of the IEEE 5th International Conference on Cloud Computing (CLOUD), 678–685 (2012)

    Google Scholar 

  21. Wu, Z., Xu, Z., Wang, H.: Whispers in the hyper-space: high-speed covert channel attacks in the cloud. In: Proceedings of the 21st USENIX Conference on Security Symposium, Security’12, 9–9, Berkeley, USA (2012). (USENIX Association)

    Google Scholar 

  22. Xiao, J., Xu, Z., Huang, H., Wang, H.: Security implications of memory deduplication in a virtualized environment. In: Proceedings of the 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 1–12 (2013)

    Google Scholar 

  23. Xu, Y., Bailey, M., Jahanian, F., Joshi, K., Hiltunen, M., Schlichting, R.: An exploration of l2 cache covert channels in virtualized environments. In: Proceedings of the 3rd ACM Workshop on Cloud Computing Security Workshop, CCSW ’11, 29–40, New York, USA (2011). (ACM)

    Google Scholar 

Download references

Acknowledgments

This research was supported by the Helmholtz Research School on Security Technologies.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to J.-P. Seifert .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Peter, M., Petschick, M., Vetter, J., Nordholz, J., Danisevskis, J., Seifert, JP. (2016). Undermining Isolation Through Covert Channels in the Fiasco.OC Microkernel. In: Abdelrahman, O., Gelenbe, E., Gorbil, G., Lent, R. (eds) Information Sciences and Systems 2015. Lecture Notes in Electrical Engineering, vol 363. Springer, Cham. https://doi.org/10.1007/978-3-319-22635-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-22635-4_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-22634-7

  • Online ISBN: 978-3-319-22635-4

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics