- PPL-devel - BUGSENG Mailman

visualizing polyhedra
by Piotr Mardziel 08 Jan '14

08 Jan '14

Hello ppl developers. I’m trying to visualize (draw) polyhedra but am finding it hard to do so with the representations provided in ppl. Is there some reasonable way to get from ppl or (easily) compute the faces of a polyhedron so that it can be drawn? Best, Piotr (Peter) Mardziel <piotrm(a)cs.umd.edu> http://www.cs.umd.edu/~piotrm

2 1

[GIT] ppl/ppl(master): Fixed HenryMM12b.
by Roberto Bagnara 05 Jan '14

05 Jan '14

Module: ppl/ppl Branch: master Commit: 530ee7a5bebed7f8eba0d0895abe68282df4fe59 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=530ee7a5bebe… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Jan 5 12:58:34 2014 +0100 Fixed HenryMM12b. --- doc/ppl_citations.bib | 5 +++-- 1 files changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 995ce7a..f8faf73 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3100,9 +3100,10 @@ Summarizing: @Article{HenryMM12b, Author = "J. Henry and D. Monniaux and M. Moy", - Title = "{PAGAI}: a path sensitive static analyzer", + Title = "{PAGAI}: A Path Sensitive Static Analyzer", Journal = "Electronic Notes in Theoretical Computer Science", - Publisher = "Elsevier Science Publishers B.V. Amsterdam, The Netherlands", + Publisher = "Elsevier Science Publishers B.V.", + Address = "Amsterdam, The Netherlands", Volume = 289, Year = 2012, ISSN = "1571-0661",

1 0

[GIT] ppl/ppl(master): Reference added.
by Patricia Hill 04 Jan '14

04 Jan '14

Module: ppl/ppl Branch: master Commit: 50a8c521d0fd13b0bb4f09d0a670e4e2d79ee2a7 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=50a8c521d0fd… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sat Jan 4 07:09:46 2014 +0000 Reference added. --- doc/ppl_citations.bib | 27 ++++++++++++++++++++++++++- 1 files changed, 26 insertions(+), 1 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 4293763..995ce7a 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3064,7 +3064,7 @@ Summarizing: been made available online for demonstration." } -@Inproceedings{HenryMM12, +@Inproceedings{HenryMM12a, Author = "J. Henry and D. Monniaux and M. Moy", Title = "Succinct Representations for Abstract Interpretation", Booktitle = "Static Analysis: @@ -3098,6 +3098,31 @@ Summarizing: ones, on a variety of open-source packages." } +@Article{HenryMM12b, + Author = "J. Henry and D. Monniaux and M. Moy", + Title = "{PAGAI}: a path sensitive static analyzer", + Journal = "Electronic Notes in Theoretical Computer Science", + Publisher = "Elsevier Science Publishers B.V. Amsterdam, The Netherlands", + Volume = 289, + Year = 2012, + ISSN = "1571-0661", + Pages = "15--25", + Abstract = "We describe the design and the implementation of PAGAI, + a new static analyzer working over the LLVM compiler + infrastructure, which computes inductive invariants on + the numerical variables of the analyzed program. PAGAI + implements various state-of-the-art algorithms combining + abstract interpretation and decision procedures + (SMT-solving), focusing on distinction of paths inside + the control flow graph while avoiding systematic + exponential enumerations. It is parametric in the + abstract domain in use, the iteration algorithm, and the + decision procedure. We compared the time and precision + of various combinations of analysis algorithms and + abstract domains, with extensive experiments both on + personal benchmarks and widely available GNU programs." +} + @Inproceedings{HoweK12, Author = "J. M. Howe and A. King", Title = "Polyhedral Analysis Using Parametric Objectives",

1 0

[GIT] ppl/ppl(master): Extended copyright years.
by Roberto Bagnara 01 Jan '14

01 Jan '14

1 0

[GIT] ppl/ppl(master): Several corrections.
by Roberto Bagnara 30 Dec '13

30 Dec '13

Module: ppl/ppl Branch: master Commit: fdae6f8ee33043bd31efd02fc5246777043a36cc URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fdae6f8ee330… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Dec 30 09:35:32 2013 +0100 Several corrections. --- doc/ppl_citations.bib | 17 ++++++++--------- 1 files changed, 8 insertions(+), 9 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 8d0974e..8ede7c8 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3733,15 +3733,15 @@ Summarizing: to no loss in precision." } -@Inproceedings{MardzielMMS11, - Title = "Dynamic Enforcement of Knowledge-based Security Policies", +@Inproceedings{MardzielMHS11, Author = "P. Mardziel and S. Magill and M. Hicks and M. Srivatsa", + Title = "Dynamic Enforcement of Knowledge-based Security Policies", Year = 2011, Booktitle = "Proceedings of the 24th IEEE Computer Security - Foundations Symposium ({CSF})", + Foundations Symposium (CSF 2011)", Publisher = "IEEE Xplore Digital Library", - Address = "New Orleans, Louisiana, USA", - Editor = "M. Backes and S.Zdancewic", + Address = "Cernay-la-Ville, France", + Editor = "M. Backes and S. Zdancewic", Pages = "114--128", ISBN = "978-0-7695-4365-9", Abstract = "This paper explores the idea of knowledge-based security @@ -4407,11 +4407,10 @@ Summarizing: } @Inproceedings{RastogiMMH13, Author = "A. Rastogi and P. Mardziel and M. Hammer and M. Hicks", - Title = "Knowledge Inference for Optimizing Secure Multi-party Computation", + Title = "Knowledge Inference for Optimizing Secure Multi-Party Computation", Year = 2013, - Booktitle = "{PLAS} '13: - Proceedings of the Eighth ACM SIGPLAN Workshop on - Programming Languages and Analysis for Security", + Booktitle = "Proceedings of the 2013 ACM SIGPLAN Workshop on + Programming Languages and Analysis for Security (PLAS'13)", Editor = "P. Naldurg", ISBN = "978-1-4503-2144-0", Address = "Seattle, Washington, USA",

1 0

[GIT] ppl/ppl(master): Capitalization fixes.
by Roberto Bagnara 30 Dec '13

30 Dec '13

Module: ppl/ppl Branch: master Commit: 7b0e718dfc86e8b3a4e9e467923efb4dcbb7b62c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=7b0e718dfc86… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Mon Dec 30 08:47:22 2013 +0100 Capitalization fixes. --- doc/ppl_citations.bib | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 08774df..8d0974e 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3586,7 +3586,7 @@ Summarizing: @Article{LimeMR13, Author = "D. Lime and C. Martinez and O. H. Roux", - Title = "Shrinking of Time Petri nets", + Title = "Shrinking of Time {Petri} Nets", Journal = "Discrete Event Dynamic Systems", Publisher = "Springer-Verlag, Berlin", Volume = 23, @@ -5040,7 +5040,7 @@ Summarizing: @Article{TraonouezLR09, Author = "L.-M. Traonouez and D. Lime and O. H. Roux", - Title = "Parametric Model-Checking of Stopwatch Petri Nets", + Title = "Parametric Model-Checking of Stopwatch {Petri} Nets", Journal = "Journal of Universal Computer Science", Year = 2009, Volume = 15,

1 0

[GIT] ppl/ppl(master): Reference added.
by Patricia Hill 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: cd637456d40bd723746f31594b553e0fa6a66aa5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=cd637456d40b… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sun Dec 29 21:52:42 2013 +0000 Reference added. --- doc/ppl_citations.bib | 36 ++++++++++++++++++++++++++++++++++++ 1 files changed, 36 insertions(+), 0 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index e78fcf9..08774df 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -3733,6 +3733,42 @@ Summarizing: to no loss in precision." } +@Inproceedings{MardzielMMS11, + Title = "Dynamic Enforcement of Knowledge-based Security Policies", + Author = "P. Mardziel and S. Magill and M. Hicks and M. Srivatsa", + Year = 2011, + Booktitle = "Proceedings of the 24th IEEE Computer Security + Foundations Symposium ({CSF})", + Publisher = "IEEE Xplore Digital Library", + Address = "New Orleans, Louisiana, USA", + Editor = "M. Backes and S.Zdancewic", + Pages = "114--128", + ISBN = "978-0-7695-4365-9", + Abstract = "This paper explores the idea of knowledge-based security + policies, which are used to decide whether to answer + queries over secret data based on an estimation of the + querier's (possibly increased) knowledge given the + results. Limiting knowledge is the goal of existing + information release policies that employ mechanisms such + as noising, anonymization, and + redaction. Knowledge-based policies are more general: + they increase flexibility by not fixing the means to + restrict information flow. We enforce a knowledge-based + policy by explicitly tracking a model of a querier's + belief about secret data, represented as a probability + distribution, and denying any query that could increase + knowledge above a given threshold. We implement query + analysis and belief tracking via abstract interpretation + using a novel probabilistic polyhedral domain, whose + design permits trading off precision with performance + while ensuring estimates of a querier's knowledge are + sound. Experiments with our implementation show that + several useful queries can be handled efficiently, and + performance scales far better than would more standard + implementations of probabilistic computation based on + sampling." +} + @Inproceedings{ManevichSRF04, Author = "R. Manevich and M. Sagiv and G. Ramalingam and J. Field", Title = "Partially Disjunctive Heap Abstraction",

1 0

[GIT] ppl/ppl(master): References added.
by Patricia Hill 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 71413b47572fb435f2abb2f0e29925886975ce83 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=71413b47572f… Author: Patricia Hill <patricia.hill(a)bugseng.com> Date: Sun Dec 29 21:48:34 2013 +0000 References added. --- doc/ppl_citations.bib | 168 +++++++++++++++++++++++++++++++++++++----------- 1 files changed, 129 insertions(+), 39 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=71413b47…

1 0

[GIT] ppl/ppl(master): Several corrections to the abstract of Fu13th.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: debbd4bf3e4b44a951b547a647d9d52cbe0c19e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=debbd4bf3e4b… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 17:26:25 2013 +0100 Several corrections to the abstract of Fu13th. --- doc/ppl_citations.bib | 12 ++++++------ 1 files changed, 6 insertions(+), 6 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index deaa40f..5797b6f 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2245,7 +2245,7 @@ Summarizing: Year = 2013, Abstract = "The fast and furious pace of change in computing technology has become an article of faith for many. The - reliability of computer-based systems cru- cially + reliability of computer-based systems crucially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis @@ -2253,24 +2253,24 @@ Summarizing: numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the - concept of numerical abstract domains. Unfor- tunately, + concept of numerical abstract domains. Unfortunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have - been intensively studied to an- alyze pointer behaviors + been intensively studied to analyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static - numerical anal- ysis is prototyped using the SOOT + numerical analysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of - the com- bination of the points-to analysis with another + the combination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some - pro- gram control point if they hold equal reference + program control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The

1 0

[GIT] ppl/ppl(master): Added abstract of Fu13th.
by Roberto Bagnara 29 Dec '13

29 Dec '13

Module: ppl/ppl Branch: master Commit: 0032c63a93d8d7ca1330fb796d4c802f9766f1aa URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0032c63a93d8… Author: Roberto Bagnara <roberto.bagnara(a)bugseng.com> Date: Sun Dec 29 12:21:25 2013 +0100 Added abstract of Fu13th. --- doc/ppl_citations.bib | 58 ++++++++++++++++++++++++++++++++++++++---------- 1 files changed, 46 insertions(+), 12 deletions(-) diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib index 9c0fa83..deaa40f 100644 --- a/doc/ppl_citations.bib +++ b/doc/ppl_citations.bib @@ -2233,6 +2233,52 @@ Summarizing: system benchmark from the literature." } +@PhDThesis{Fu13th, + Title = "Static Analysis of Numerical Properties in the Presence of Pointers", + Author = "Z. Fu", + Type = "Th\`{e}se pour le grade de + {``Docteur de l'Universit\'e de Rennes 1''}", + School = "\'{E}cole doctorale MATISSE, Universit\'{e} de Rennes 1 + sous le sceau de l'Universit\'e Europ\'eenne de Bretagne", + Address = "Rennes, France", + Month = dec, + Year = 2013, + Abstract = "The fast and furious pace of change in computing + technology has become an article of faith for many. The + reliability of computer-based systems cru- cially + depends on the correctness of its computing. Can man, + who created the computer, be capable of preventing + machine-made misfortune? The theory of static analysis + strives to achieve this ambition. The analysis of + numerical properties of programs has been an essential + research topic for static analysis. These kinds of + properties are commonly modeled and handled by the + concept of numerical abstract domains. Unfor- tunately, + lifting these domains to heap-manipulating programs is + not obvious. On the other hand, points-to analyses have + been intensively studied to an- alyze pointer behaviors + and some scale to very large programs but without + inferring any numerical properties. We propose a + framework based on the theory of abstract interpretation + that is able to combine existing numerical domains and + points-to analyses in a modular way. The static + numerical anal- ysis is prototyped using the SOOT + framework for pointer analyses and the PPL library for + numerical domains. The implementation is able to analyze + large Java program within several minutes. The second + part of this thesis consists of a theoretical study of + the com- bination of the points-to analysis with another + pointer analysis providing information called + must-alias. Two pointer variables must alias at some + pro- gram control point if they hold equal reference + whenever the control point is reached. We have developed + an algorithm of quadruple complexity that sharpens + points-to analysis using must-alias information. The + algorithm is proved correct following a semantics-based + formalization and the concept of bisimulation borrowed + from the game theory, model checking etc." +} + @Inproceedings{Fu14a, Author = "Z. Fu", Title = "Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java", @@ -2285,18 +2331,6 @@ Summarizing: scalability." } -@PhDThesis{Fu13th, - Title = "Static Analysis of Numerical Properties in the Presence of Pointers", - Author = "Z. Fu", - Type = "Th\`{e}se pour le grade de - {``Docteur de l'Universit\'e de Rennes 1''}", - School = "\'{E}cole doctorale MATISSE, Universit\'{e} de Rennes 1 - sous le sceau de l'Universit\'e Europ\'eenne de Bretagne", - Address = "Rennes, France", - Month = dec, - Year = 2013, -} - @Article{GallardoP13, Author = "M.-d.-M. Gallardo and L. Panizo", Title = "Extending Model Checkers for Hybrid System Verification:

1 0