Abstract
Memory safety breaches have been main tools in many of the latest security vulnerabilities. Therefore memory safety is critical and attractive property for any piece of code. Separation logic can be realized as a mathematical tool to reason about memory safety of programs. An important technique for modern parallel programming is multithreading. For a multi-threaded model of programming (Core-Par-C), this paper introduces an accurate semantics which is employed to mathematically prove the undecidability of memory-safety of Core-Par-C programs. The paper also proposes a design for a hardware to act as an efficient memory checker against memory errors.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Abdulla, P.A., Dwarkadas, S., Rezine, A., Shriraman, A., Zhu, Y.: Verifying safety and liveness for the flextm hybrid transactional memory. In: Macii, E. (ed.) Design, Automation and Test in Europe, DATE 13, Grenoble, France, March 18–22, 2013, pp. 785–790. EDA Consortium San Jose, CA, USA / ACM DL (2013)
Austin, T.M., Breach, S.E., Sohi, G.S.: Efficient detection of all pointer and array access errors. In: Sarkar, V., Ryder, B.G., Soffa, M.L. (eds.) PLDI, pp. 290–301. ACM (1994)
Baker, J., Cunei, A., Kalibera, T., Pizlo, F., Vitek, J.: Accurate garbage collection in uncooperative environments revisited. Concurrency and Computation: Practice and Experience 21(12), 1572–1606 (2009)
Bensalem, S., Peled, D. (eds): Runtime Verification. 9th International Workshop, RV 2009, Grenoble, France, June 26–28, 2009. Selected Papers, volume 5779 of Lecture Notes in Computer Science. Springer (2009)
Berger, E.D., Zorn, B.G.: Diehard: probabilistic memory safety for unsafe languages. In: Schwartzbach, M.I., Ball, T. (eds) PLDI, pp. 158–168. ACM (2006)
Chatterjee, K., Prabhu, V.S.: Synthesis of memory-efficient, clock-memory free, and non-zeno safety controllers for timed systems. Inf. Comput. 228, 83–119 (2013)
Damm, W., Dierks, H., Oehlerking, J., Pnueli, A.: Towards Component Based Design of Hybrid Systems: Safety and Stability. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol. 6200, pp. 96–143. Springer, Heidelberg (2010)
Dhurjati, D., Adve, V.S.: Efficiently detecting all dangling pointer uses in production servers. In: DSN, pp. 269–280. IEEE Computer Society (2006)
Dhurjati, D., Kowshik, S., Adve, V.S., Lattner, C.: Memory safety without runtime checks or garbage collection. In: Mueller, F., Kremer, U. (eds.) LCTES, pp. 69–80. ACM (2003)
Dillig, T., Dillig, I., Chaudhuri, S.: Optimal guard synthesis for memory safety. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 491–507. Springer, Heidelberg (2014)
Godefroid, P., Kinder, J.: Proving memory safety of floating-point computations by combining static and dynamic program analysis. In: Tonella, P., Orso, A. (eds.), Proceedings of the Nineteenth International Symposium on Software Testing and Analysis, ISSTA 2010, Trento, Italy, July 12–16, 2010, pp. 1–12. ACM (2010)
Grossman, D., Morrisett, J.G., Jim, T., Hicks, M.W., Wang, Y., Cheney, J.: Region-based memory management in cyclone. In: Knoop, J., Hendren, L.J. (eds.) PLDI, pp. 282–293. ACM (2002)
Hertz, M., Berger, E.D.: Quantifying the performance of garbage collection vs. explicit memory management. In: Johnson, R.E., Gabriel, R.P. (eds.) OOPSLA, pp. 313–326. ACM (2005)
Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: A safe dialect of c. In: Ellis, C.S. (ed.) USENIX Annual Technical Conference, General Track, pages 275–288. USENIX (2002)
Rogers Jr, H.: Theory of Recursive Functions and Effective Computability. MIT press, Cambridge, MA (1987)
Lamport, L.: The hoare logic’ of concurrent programs. Acta Inf. 14, 21–37 (1980)
Lee, H.-C., Seong, P.-H.: A computational model for evaluating the effects of attention, memory, and mental models on situation assessment of nuclear power plant operators. Rel. Eng. & Sys. Safety 94(11), 1796–1805 (2009)
Li, H., Gao, H., Shi, P., Zhao, X.: Fault-tolerant control of markovian jump stochastic systems via the augmented sliding mode observer approach. Automatica 50(7), 1825–1834 (2014)
Marriott, C., Cavalcanti, A.: SCJ: memory-safety checking without annotations. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 465–480. Springer, Heidelberg (2014)
Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Watchdog: Hardware for safe and secure manual memory management and full memory safety. In: 39th International Symposium on Computer Architecture (ISCA 2012), June 9–13, 2012, Portland, OR, USA, pp. 189–200. IEEE (2012)
Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: Ccured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst. 27(3), 477–526 (2005)
Necula, G.C., McPeak, S., Weimer, W.: Ccured: type-safe retrofitting of legacy code. In: Launchbury, J., Mitchell, J.C. (eds.) POPL, pp. 128–139. ACM (2002)
Oiwa, Y.: Implementation of the memory-safe full ansi-c compiler. In: Hind, M., Diwan, A. (eds) PLDI, pp. 259–269. ACM (2009)
Patil, H., Fischer, C.N.: Low-cost, concurrent checking of pointer and array accesses in c programs. Softw., Pract. Exper. 27(1), 87–110 (1997)
Qin, F., Tucek, J., Zhou, Y., Sundaresan, J.: Rx: Treating bugs as allergies - a safe method to survive software failures. ACM Trans. Comput. Syst. 25(3) (2007)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22–25 July 2002, Copenhagen, Denmark, Proceedings, pp. 55–74. IEEE Computer Society (2002)
Rinard, M.C., Cadar, C., Dumitran, D., Roy, D.M., Leu,T., Beebee, W.S.: Enhancing server availability and security through failure-oblivious computing. In: Brewer, E.A., Chen, P. (eds.) OSDI, pp. 303–316. USENIX Association (2004)
Rosu, G., Schulte, W., Serbanuta, T.-F.: Runtime verification of c memory safety. In: Bensalem and Peled [4], pp. 132–151
Simpson, M.S., Barua, R.: Memsafe: ensuring the spatial and temporal memory safety of c at runtime. Softw., Pract. Exper. 43(1), 93–128 (2013)
Singh, A., Narayanasamy, S., Marino, D., Millstein, T.D., Musuvathi, M.: A safety-first approach to memory models. IEEE Micro 33(3), 96–104 (2013)
Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 208–223. Springer, Heidelberg (2014)
Vazou, N., Papakyriakou, M.A., Papaspyrou, N.: Memory safety and race freedom in concurrent programming languages with linear capabilities. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Federated Conference on Computer Science and Information Systems - FedCSIS 2011, Szczecin, Poland, 18–21 September 2011, Proceedings, pp. 833–840 (2011)
Xu, W., DuVarney, D.C., Sekar, R.: An efficient and backwards-compatible transformation to ensure memory safety of c programs. In: Taylor, R.N., Dwyer, M.B. (eds.) SIGSOFT FSE, pp. 117–126. ACM (2004)
Yang, J., Cui, H., Jingyue, W., Tang, Y., Gang, H.: Making parallel programs reliable with stable multithreading. Commun. ACM 57(3), 58–69 (2014)
Yong, S.H., Horwitz, S.: Protecting c programs from attacks via invalid pointer dereferences. In: ESEC / SIGSOFT FSE, pp. 307–316. ACM (2003)
Zorn, B.G.: The measured cost of conservative garbage collection. Softw., Pract. Exper. 23(7), 733–756 (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
El-Zawawy, M.A. (2015). Novel Designs for Memory Checkers Using Semantics and Digital Sequential Circuits. In: Gervasi, O., et al. Computational Science and Its Applications -- ICCSA 2015. ICCSA 2015. Lecture Notes in Computer Science(), vol 9158. Springer, Cham. https://doi.org/10.1007/978-3-319-21410-8_46
Download citation
DOI: https://doi.org/10.1007/978-3-319-21410-8_46
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21409-2
Online ISBN: 978-3-319-21410-8
eBook Packages: Computer ScienceComputer Science (R0)