Exhaustive website verifier

Question

I have this grand idea to basically employ some brute force attack to test/verify that my web application doesn't crash.

Don't get me started on unit testing, and IoC stuff, this is something else entirely.

What I'm doing, and what I'm asking for help with is to create an intelligent exhaustive search, that explore parts of the program state.

What I have is a web page with things I can do, clicking is one thing, text input is another, some inputs like radio buttons and drop down lists are constrained to certain values. Pretty basic things. What I end up with a finite set of events and values and what I want to model is a progression of state. Maybe this is FSM optimization in a way, but the goal is to systematically go through arbitrary permutations of events and values and see what happens.

When a problem is found I want to try and provoke that error with as little effort as possible to be able to present a clear test case.

This relates to formal verification methods and I'm asking for help or insight from people with experience.

Answer 1

What you want to do sounds a little like model-checking, on the one hand, and automated test case generation on the other hand (in the latter category check out Concolic testing, a technique to avoid wasting time with unfeasible execution paths).

Model-checking would be the preferred method if you assume your web application is correct and want to prove that it is. But in the case of a warning, you may have to work to understand if the problem is real or not. Test case generation is oriented towards bug-finding: it does not prove that you app is correct, but if it finds a problem, it gives you an input vector to produce it so you don't need to wonder if the problem is real.

I am not aware of any existing tools for web apps, but that doesn't mean that they don't exist.

Answer 2

It sounds like you want a fuzzer. Peach is one such tool.

Answer 3

Exhaustive search can be non trivial task for limited resource (memory,space) ,but with many techniques the problem can be reduced ,like abstracting you code (ex: replacing database driver classes with stubs), an experience is presented in this paper: Abstract Model Checking of Web Applications Using Java PathFinder (Vinh Cuong Tran, Yoshinori Tanabe, Masami Hagiya, University of Tokyo).

If you look to a kind of formal verification of FSM like models, Java PathFinder has an extension to verify UML state charts written in Java+annotation (it depends on the Javapathfinder VM):

http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-statechart