Skip to main content
SpringerLink
Log in

Equivalence of Finite-Valued Symbolic Finite Transducers

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9609))

Abstract

Symbolic Finite Transducers, or SFTs, is a representation of finite transducers that annotates transitions with logical formulas to denote sets of concrete transitions. This representation has practical advantages in applications for web security analysis, where it provides ways to succinctly represent web sanitizers that operate on large alphabets. More importantly, the representation is also conducive for efficient analysis using state-of-the-art theorem proving techniques. Equivalence checking plays a central role in deciding properties of SFTs such as idempotence and commutativity. We show that equivalence of finite-valued SFTs is decidable, i.e., when the number of possible outputs for a given input is bounded by a constant.

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.

    Definition 4 is consistent with [4, 5]. However, the definition of a GSM is not standardized in the literature. Some sources define GSMs without a dedicated set of final states [6].

References

  1. Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with Bek. In: USENIX Security, pp. 1–16 (2011)

    Google Scholar 

  2. Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bjorner, N.: Symbolic finite state transducers: Algorithms and applications. In: POPL 2012. ACM, pp. 137–150 (2012)

    Google Scholar 

  3. Balzarotti, D., Cova, M., Felmetsger, V., Jovanovic, N., Kirda, E., Kruegel, C., Vigna, G.: Saner: Composing static and dynamic analysis to validate sanitization in web applications. In: SP (2008)

    Google Scholar 

  4. Yu, S.: Regular languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 1, pp. 41–110. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  5. Demers, A., Keleman, C., Reusch, B.: On some decidable properties of finite state translations. Acta Informatica 17, 349–364 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  6. Harrison, M.A.: Introduction to Formal Language Theory. Addison-Wesley, Reading (1978)

    MATH  Google Scholar 

  7. Bjørner, N., Veanes, M.: Symbolic transducers. Microsoft Research, Technical Report MSR-TR-2011-3 (2011)

    Google Scholar 

  8. Ibarra, O.: The unsolvability of the equivalence problem for Efree NGSM’s with unary input (output) alphabet and applications. SIAM J. Comput. 4, 524–532 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  9. Schützenberger, M.P.: Sur les relations rationnelles. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol. 33, pp. 209–213. Springer, Heidelberg (1975)

    Google Scholar 

  10. Culic, K., Karhumäki, J.: The equivalence problem for single-valued two-way transducers (on NPDT0L languages) is decidable. SIAM J. Comput. 16(2), 221–230 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  11. Weber, A.: Decomposing finite-valued transducers and deciding their equivalence. SIAM J. Comput. 22(1), 175–202 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  12. D’Antoni, L., Veanes, M.: Equivalence of extended symbolic finite transducers. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 624–639. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. Minamide, Y.: Static approximation of dynamically generated web pages. In: Proceedings of the 14th International Conference on the World Wide Web, WWW 2005, pp. 432–441 (2005)

    Google Scholar 

  14. Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: PLDI, pp. 32–41. ACM (2007)

    Google Scholar 

  15. Wassermann, G., Yu, D., Chander, A., Dhurjati, D., Inamura, H., Su, Z.: Dynamic test input generation for web applications. In: ISSTA (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Redmond, USA

    Margus Veanes & Nikolaj Bjørner

Authors
  1. Margus Veanes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nikolaj Bjørner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Margus Veanes .

Editor information

Editors and Affiliations

  1. Innopolis University, Innopolis, Russia

    Manuel Mazzara

  2. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Veanes, M., Bjørner, N. (2016). Equivalence of Finite-Valued Symbolic Finite Transducers. In: Mazzara, M., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2015. Lecture Notes in Computer Science(), vol 9609. Springer, Cham. https://doi.org/10.1007/978-3-319-41579-6_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-41579-6_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-41578-9

  • Online ISBN: 978-3-319-41579-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation