Skip to main content
SpringerLink
Log in

Processor Rescue

Safe Coding for Hardware Aliasing

  • Conference paper
  • First Online:
Book cover Intelligent Software Methodologies, Tools and Techniques (SoMeT 2015)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 532))

Abstract

What happens if a Mars lander takes a cosmic ray through the processor and thereafter \(1\,\mathtt{+ }\,1=3\)? Coping with the fault is feasible but requires the numbers 2 and 3 to be treated as indistinguishable for the purposes of arithmetic, while as memory addresses they continue to access different memory cells. If a program is to run correctly in this altered environment it must be prepared to see address 2 sporadically access data in memory cell 3, which is known as ‘hardware aliasing’. This paper describes a programming discipline that allows software to run correctly in a hardware aliasing context, provided the aliasing is underpinned by hidden determinism.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight 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

Institutional subscriptions

Notes

  1. 1.

    The Curiosity rover now on Mars has a second processor that was signalled to take over on February 28, 2013, due to an issue with the active processor’s flash memory that resulted in it continuously rebooting, draining power. The rover was not heard from again until March 4, the spacecraft nearly having been lost. The issue reoccurred late in March, 2013, and full normal operation was only finally resumed on March 25, 2013, after reloading programs to a different portion of flash memory.

  2. 2.

    Barr in [2] describes it thus: “Hardware Aliasing: ...[is] used to describe the situation where, due to either a hardware design choice or a hardware failure, one or more of the available address bits is not used in the memory selection process.” That is, the available memory address bits do not serve to distinguish two different locations.

  3. 3.

    A more sophisticated version of this recipe relaxes the rule to allow different aliases than 0xabcd to be used provided that the same alias is always used for one write and the succeeding reads; the next write may use a different alias again.

References

  1. Allen, R., Kennedy, K.: Optimizing Compilers for Modern Architectures: A Dependence-Based Approach, vol. 289. Morgan Kaufmann, San Francisco (2002)

    MATH  Google Scholar 

  2. Barr, M.: Programming Embedded Systems in C and C++, 1st edn. O’Reilly & Associates Inc., Sebastopol (1998)

    Google Scholar 

  3. Bowen, J.P., Breuer, P.T.: Decompilation. In: van Zuylen, H. (ed.) The REDO Compendium: Reverse Engineering for Software Maintenance, chap. 10, pp. 131–138. John Wiley & Sons, Hoboken (1993)

    Google Scholar 

  4. Breuer, P.T., Bowen, J.P.: Decompilation: the enumeration of types and grammars. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1613–1647 (1994)

    Article  Google Scholar 

  5. Breuer, P.T., Bowen, J.P.: Typed assembler for a RISC crypto-processor. In: Barthe, G., Livshits, B., Scandariato, R. (eds.) ESSoS 2012. LNCS, vol. 7159, pp. 22–29. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Breuer, P.T., Bowen, J.P.: Certifying machine code safe from hardware aliasing: RISC is not necessarily risky. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 371–388. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  7. Breuer, P.T., Bowen, J.P.: A fully homomorphic crypto-processor design. In: Jürjens, J., Livshits, B., Scandariato, R. (eds.) ESSoS 2013. LNCS, vol. 7781, pp. 123–138. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Breuer, P.T., Bowen, J.P.: Avoiding hardware aliasing: verifying RISC machine and assembly code for encrypted computing. In: Proceedings of the 25th IEEE Intlernational Symposium on Software Reliability Engineering Workshops (ISSRE 2014), 2nd IEEE International Workshop on Reliability and Security Data Analysis (RSDA 2014), pp. 365–370. IEEE, November 2014

    Google Scholar 

  9. Breuer, P.T., Bowen, J.P.: Towards a working fully homomorphic crypto-processor. In: Jürjens, J., Piessens, F., Bielova, N. (eds.) ESSoS. LNCS, vol. 8364, pp. 131–140. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  10. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Glosserman, P.: Quarterdeck Expanded Memory Manager: QEMM, Instant Power for 386, 486 or Pentium PCs. Quarterdeck Office Systems, Santa Monica (1985)

    Google Scholar 

  12. Gruhn, M., Müller, T.: On the practicability of cold boot attacks. In: 8th International Conference on Availability, Reliability and Security (ARES 2013), pp. 390–397, September 2013

    Google Scholar 

  13. Halderman, J.A., Schoen, S.D., Heninger, N., Clarkson, W., Paul, W., Calandrino, J.A., Feldman, A.J., Appelbaum, J., Felten, E.W.: Lest we remember: cold-boot attacks on encryption keys. Commun. ACM 52(5), 91–98 (2009)

    Article  Google Scholar 

  14. He, J., Bowen, J.P.: Specification, verification and prototyping of an optimized compiler. Formal Aspects Comput. 6(6), 643–658 (1994)

    Article  MATH  Google Scholar 

  15. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

  16. Patterson, D.A.: Reduced instruction set computers. Commun. ACM 28(1), 8–21 (1985)

    Article  Google Scholar 

  17. Simmons, P.: Security through amnesia: a software-based solution to the cold boot attack on disk encryption. In: Proceedings of the 27th Annual Computer Security Applications Conference (ACSAC 2011), pp. 73–82. ACM, New York (2011)

    Google Scholar 

  18. Tsoutsos, N.G., Maniatakos, M.: The HEROIC framework: encrypted computation without shared keys. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 34(6), 875–888 (2015)

    Article  Google Scholar 

  19. Wang, S., Hu, J., Ziavras, S.G.: On the characterization of data cache vulnerability in high-performance embedded microprocessors. In: Proceedings of the IC-SAMOS 2006: International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation, pp. 14–20, July 2006

    Google Scholar 

Download references

Acknowledgements

Simon Pickin’s contribution to the research described in this paper has been partially supported by the Spanish MEC project ESTuDIo (TIN2012-36812-C02-01). Peter T. Breuer wishes to acknowledge the support of HecuSys Inc. (http://www.hecusys.com) in connection with KPU technology, described herein.

Author information

Authors and Affiliations

  1. School of Computing, Telecommunications and Networks, Birmingham City University, Birmingham, UK

    Peter T. Breuer & Jonathan P. Bowen

  2. Facultad de Informática, Complutense University of Madrid, Madrid, Spain

    Simon Pickin

Authors
  1. Peter T. Breuer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jonathan P. Bowen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Simon Pickin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Peter T. Breuer .

Editor information

Editors and Affiliations

  1. Iwate Prefectural University, Takizawa, Japan

    Hamido Fujita

  2. University of Naples "Federico II", Napoli, Italy

    Guido Guizzi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Breuer, P.T., Bowen, J.P., Pickin, S. (2015). Processor Rescue. In: Fujita, H., Guizzi, G. (eds) Intelligent Software Methodologies, Tools and Techniques. SoMeT 2015. Communications in Computer and Information Science, vol 532. Springer, Cham. https://doi.org/10.1007/978-3-319-22689-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-22689-7_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-22688-0

  • Online ISBN: 978-3-319-22689-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation