Static analysis for reasoning about security-related properties

Ana Milanova
Renselaer Polytechnic Institute
http://www.cs.rpi.edu/~milanova/

Abstract: 

It is well-known that reasoning about ownership, immutability and
information flows can help prevent serious security-related program
flaws.

We propose a practical approach towards reasoning about these
properties: it is based on the UML and light-weight static
analysis. Specifically, we propose the use of ownership, immutability
and information flow constraints on UML design class diagrams. These
constraints impose requirements on the implementation; the constraints
can be verified through static analysis incorporated within a
reverse-engineering tool for UML class diagrams.

This talk focuses on the ownership, immutability and information flow
analyses that we have developed for this purpose. The analyses do not
require annotations, and are practical and precise. We believe that
they can be incorporated in reverse engineering tools, and can help
support practical and effective verification and reasoning about
security-related properties.

(joint work with Yin Liu)