VERIFICATION TECHNIQUES AND TOOLS FOR SOFTWARE SECURITY
January 04, 2021
It is hard to ensure that complex software combining data, functionality, and multitenancy (e.g. web applications) is trustworthy, and efforts are being made to empower developers with automated verification techniques making sure that no security flaws are introduced at development time, as is often the case. We are developing language-based techniques to tackle this issue, focusing on privacy and security, and live evolution, in complex scenarios where security levels dynamically depend on data being manipulated. Our results include novel static analyses for privacy and confidentiality in data centric apps. We have also recently introduced results on type based information flow analysis for dynamic data dependencies, leading to a prototype publicly available at Microsoft Research Rise4Fun. Results have led to a US patent with OutSystems SA on model-driven security, to several PhD and MSc thesis, with fundamental results being published at top conferences such as POPL and ESOP.
