Description
Modern software systems often process data subject to specific usage policies that
define how and under what conditions information may be handled. While conceptual
models for such usage control requirements are well established, practical methods for
verifying their enforcement remain limited. Traditional techniques, such as fingerprinting
methods, that involve hashing of application states or snapshots are fragile, require
manual review, and provide little insight into the actual behavior of an application. This
thesis presents an approach for verifying usage control properties through static code
analysis using code property graphs. By enriching code property graphs with semantic
abstractions that represent key data handling operations, such as sending, persisting,
or logging, this method enables the definition of high-level, reusable analysis rules.
These rules allow for fully automated detection of potential violations without relying
on specific implementation details. The feasibility of the approach is demonstrated
through a prototype targeting Python-based web applications, with a focus on the Flask
framework. Evaluation on both controlled examples and real world applications, show
that the method can reliably assess whether usage control requirements are respected,
offering a practical and scalable approach for verifying compliance in modern software
systems.
|
Thesis topic in co-operation with the Fraunhofer Institute for Applied and Integrated Security AISEC, Garching