Microsoft Powerpoint Servlets

Static Analysis for
Java Servlets and JSP
Christian Kirkegaard
Anders Møller
BRICS, University of Aarhus

Java Servlets and JSP
A powerful framework for Web application development
Communication using HTTP:
client
server
request (URL + form fields)
response (XHTML)
JSP pages are compiled into servlets...
2 / 12

The Servlet API
A Web application contains a collection of servlets
A configuration file maps
URL requests to servlet names
Each servlet receives user input
(form fields) and produces
XHTML output
The output is generated by
printing characters to a stream!
3 / 12

Two challenges for Web app developers
1. Is the response always
well-formed and valid?
2. Do forms and fields being
generated always match
the code that receives the
input?
4 / 12

Overview of the analysis
Java code
Soot (Hendren et al.)
+ string analysis (SAS’03)
flow graph
context-free grammar
balanced grammars (Knuth)
+ much more...
grammar on tag-form
XML graph
XML Schema validation (PLAN-X’06)
5 / 12

Our results
Construction of context-free grammars
that approximate the possible output
on output streams in Java
Checks for XML well-formedness and
XML Schema validity
on context-free grammars
Inter-servlet control flow for Web apps
6 / 12

Java code
Flow graphs
flow graph
context-free grammar
Nodes:
gramma
grammar on tag-form
append[regular language]
XML graph
invoke[possible targets]
nop
return
Edges represent control flow
– Soot (Hendren et al.) gives us Jimple code,
control flow analysis, and alias analysis
– String analysis (SAS’03) gives us
a regular language for each string expression
7 / 12

Java code
Flow graphs → context-free grammars
flow graph
context-free grammar
n
gramma
grammar on tag-form
append[L]
Nn → RL Nm
XML graph
m
n
invoke[t]
Nn → Nt Nm
m
n
nop
Nn → Nm
m
n
N
return
n → ε
8 / 12

Java code
Tag-form
flow graph
context-free grammar
C → < T A > C </ T > (element)
gramma
grammar on tag-form
C → X
(text)
XML graph
C → C C
(content sequence)
A → W T = ” V ”
(attribute)
A → A A
(attribute sequence)
A → ε
(empty attr. seq.)
– if the grammar can’t be brought on this form,
its language is not well-formed XML
– on tag-form, we can easily check the remaining
properties for well-formedness...
9 / 12

Java code
Transforming to tag-form
flow graph
context-free grammar
1. make </ a single symbol
gramma
grammar on tag-form
2. obtain balanced grammar
XML graph
with respect to < and </
– Knuth ’67
– Mohri & Nederhof ’01
3. obtain unique contexts
(tag / element content / attribute value)
– if possible
4. apply standard grammar transformations
(inlining, expansion)...
10 / 12

Java code
Checking validity with XML graphs
flow graph
context-free grammar
An XML graph is like an
gramma
grammar on tag-form
XML tree but with
XML graph
• choices and loops
• attribute/element names and text described
with regular string languages
(so one XML graph represents a set of concrete XML trees)
Converting a context-free grammar on tag
form into an XML graph is straightforward
We have a tool for validating XML graphs
relative to schemas (using XML Schema)!
11 / 12

Conclusion
Construction of context-free grammars
that approximate the possible output
on output streams in Java
Java code
Sound and complete checks for
flow graph
XML well-formedness and
XML Schema validity
context-free grammar
on context-free grammars
grammar on tag-form
Inter-servlet control flow
for Servlets/JSP Web apps
XML graph
...and the implementation is on the way – reeeal soon now ☺
12 / 12