SAS 2020
Wed 18 - Fri 20 November 2020 Online Conference
co-located with SPLASH 2020
Wed 18 Nov 2020 07:40 - 08:00 at SPLASH-III - 1 Chair(s): Patrick Cousot
Wed 18 Nov 2020 19:40 - 20:00 at SPLASH-III - 1 Chair(s): Bor-Yuh Evan Chang

We present a specification language aiming at soundly modeling unavailable functions in a static analyzer for C by abstract interpretation. It takes inspiration from Behavioral Interface Specification Languages popular in deductive verification, notably Frama-C’s ACSL, as we annotate function prototypes with pre and post-conditions expressed concisely in a first-order logic, but with key differences. Firstly, the specification aims at replacing a function implementation in a safety analysis, not verifying its functional correctness. Secondly, we do not rely on theorem provers; instead, specifications are interpreted at function calls by our abstract interpreter. We implemented the language into Mopsa, a static analyzer designed to easily reuse abstract domains across widely different languages (such as C and Python). We show how its design helped us support a logic-based language with minimal effort. Notably, it was sufficient to add only a handful transfer functions (including very selective support for quantifiers) to achieve a sound and precise analysis. We modeled a large part of the GNU C library and C execution environment in our language, including the manipulation of unbounded strings, file descriptors, and programs with an unbounded number of symbolic command-line parameters, which allows verifying programs in a realistic setting. We report on the analysis of C programs from the Juliet benchmarks and Coreutils.

preprint (sas20.pdf)507KiB

Wed 18 Nov

Displayed time zone: Central Time (US & Canada) change

19:00 - 20:00
Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
Cost Analysis of Smart Contracts via Parametric Resource AnalysisInvited Talk
I: Manuel Hermenegildo IMDEA Software Institute and T.U. of Madrid
Media Attached File Attached
Research paper
A Library Modeling Language for the Static Analysis of C ProgramsArtifact
Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Media Attached File Attached