MOPS

MOPS: an infrastructure for examining security properties of software. We describe a formal approach for finding bugs in security-relevant software and verifying their absence. The idea is as follows: we identify rules of safe programming practice, encode them as safety properties, and verify whether these properties are obeyed. Because manual verification is too expensive, we have built a program analysis tool to automate this process. Our program analysis models the program to be verified as a pushdown automaton, represents the security property as a finite state automaton, and uses model checking techniques to identify whether any state violating the desired security goal is reachable in the program. The major advantages of this approach are that it is sound in verifying the absence of certain classes of vulnerabilities, that it is fully interprocedural, and that it is efficient and scalable. Experience suggests that this approach will be useful in finding a wide range of security vulnerabilities in large programs efficiently.


References in zbMATH (referenced in 22 articles )

Showing results 1 to 20 of 22.
Sorted by year (citations)

1 2 next

  1. Rinderknecht, Christian; Volanschi, Nic: Theory and practice of unparsed patterns for metacompilation (2010)
  2. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009)
  3. Bozzelli, Laura: Caret with forgettable past (2009)
  4. Güleşir, Gürcan; van den Berg, Klaas; Bergmans, Lodewijk; Akşit, Mehmet: Experimental evaluation of a tool for the verification and transformation of source code in event-driven systems (2009)
  5. Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009)
  6. Tlili, Syrine; Debbabi, Mourad: Interprocedural and flow-sensitive type analysis for memory and type safety of C code (2009)
  7. Skalka, Christian: Types and trace effects for object orientation (2008)
  8. Skalka, Christian; Smith, Scott; van Horn, David: Types and trace effects of higher order programs (2008)
  9. Udrea, Octavian; Lumezanu, Cristian; Foster, Jeffrey S.: Rule-based static analysis of network protocol implementations (2008)
  10. Volanschi, Eugen-Nicolae: A portable compiler-integrated approach to permanent checking. (2008)
  11. Volanschi, Nic: A portable compiler-integrated approach to permanent checking (2008)
  12. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007)
  13. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2006)
  14. Bouajjani, Ahmed; Esparza, Javier: Rewriting models of Boolean programs (2006)
  15. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006)
  16. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006)
  17. Beek, Maurice H.Ter; Lenzini, Gabriele; Petrocchi, Marinella: Team automata for security: - A survey -. (2005)
  18. Conway, Christopher L.; Namjoshi, Kedar S.; Dams, Dennis; Edwards, Stephen A.: Incremental algorithms for inter-procedural analysis of safety properties (2005)
  19. Reps, T.; Balakrishnan, G.; Lim, J.; Teitelbaum, T.: A next-generation platform for analyzing executables (2005)
  20. Skalka, Christian; Smith, Scott F.; Van Horn, David: A type and effect system for flexible abstract interpretation of Java: (Extended abstract). (2005)

1 2 next


Further publications can be found at: http://web.cs.ucdavis.edu/~hchen/mops/#paper