Abstract
Pushdown systems (PDSs) are a natural model for sequential programs, but they can fail to accurately represent the way an assembly stack actually operates. Indeed, one may want to access the part of the memory that is below the current stack or base pointer, hence the need for a model that keeps track of this part of the memory. To this end, we introduce pushdown systems with an upper stack (UPDSs), an extension of PDSs where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules. We prove that the sets of successors \(post^*\) and predecessors \(pre^*\) of a regular set of configurations of such a system are not always regular, but that \(post^*\) is context-sensitive, so that we can decide whether a single configuration is forward reachable or not. In order to underapproximate \(pre^*\) in a regular fashion, we consider a bounded-phase analysis of UPDSs, where a phase is a part of a run during which either push or pop rules are forbidden. We then present a method to overapproximate \(post^*\) that relies on regular abstractions of runs of UPDSs. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent.
This work was partially funded by the FUI project Freenivi.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bermudez, M.E., Schimpf, K.M.: Practical arbitrary lookahead LR parsing. J. Comput. Syst. Sci. 41, 230–250 (1990)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). doi:10.1007/3-540-63141-0_10
Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL 2003 (2003)
Carotenuto, D., Murano, A., Peron, A.: 2-visibly pushdown automata. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 132–144. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73208-2_15
Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106, 61–86 (1992)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000). doi:10.1007/10722167_20
Ginsburg, S., Greibach, S.A., Harrison, M.A.: Stack automata and compiling. J. ACM 14, 172–201 (1967)
Hopcroft, J., Ullman, J.: Sets accepted by one-way stack automata are context sensitive. Inf. Control 13, 114–133 (1968)
Pereira, F.C.N., Wright, R.N.: Finite-state approximation of phrase structure grammars. In: ACL 1991 (1991)
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31980-1_7
Seth, A.: Global reachability in bounded phase multi-stack pushdown systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 615–628. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_53
Torre, S.L., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS 2007 (2007)
Uezato, Y., Minamide, Y.: Pushdown systems with stack manipulation. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 412–426. Springer, Heidelberg (2013). doi:10.1007/978-3-319-02444-8_29
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Pommellet, A., Diaz, M., Touili, T. (2017). Reachability Analysis of Pushdown Systems with an Upper Stack. In: Drewes, F., Martín-Vide, C., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2017. Lecture Notes in Computer Science(), vol 10168. Springer, Cham. https://doi.org/10.1007/978-3-319-53733-7_33
Download citation
DOI: https://doi.org/10.1007/978-3-319-53733-7_33
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-53732-0
Online ISBN: 978-3-319-53733-7
eBook Packages: Computer ScienceComputer Science (R0)