[SystemSafety] C++ and Pointers

[Daniel Kästner]

Derek,

Astrée does a sound static analysis for defects like div/0 or buffer 
overflows. When it reports no defect, there is no defect from the defect 
classes covered by Astrée in the code.

So it's a powerful tool, and, yes, the semantical analyses of Astrée can 
take some time. Like a bit under 2 days on > 100 million lines of 
(preprocessed) code. Cf:

D. Kästner, B. Schmidt, M. Schlundt, L. Mauborgne, S. Wilhelm, C. Ferdinand. 
Analyze This! Sound Static Analysis for Integration Verification of 
Large-Scale Automotive Software. SAE Technical Paper 2019-01-1246, SAE World 
Congress 2019, Detroit, April 2019. DOI: 
https://doi.org/10.4271/2019-01-1246

Daniel.
---
Dr.-Ing. Daniel 
Kaestner --------------------------------------------------------------------
AbsInt Angewandte Informatik GmbH      Email: kaestner at AbsInt.com
Science Park 1                                                Tel: 
+49-681-3836028
66123 Saarbruecken                                     Fax: 
+49-681-3836020
GERMANY 
http://www.AbsInt.com <http://www.absint.com/>
----------------------------------------------------------------------------------------------------
Geschaeftsfuehrung: Dr.-Ing. Christian Ferdinand
Eingetragen im Handelsregister des Amtsgerichts Saarbruecken, HRB 11234


> -----Ursprüngliche Nachricht-----
> Von: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de> Im 
> Auftrag von Derek M Jones
> Gesendet: Freitag, 5. Juli 2019 14:22
> An: systemsafety at lists.techfak.uni-bielefeld.de
> Betreff: Re: [SystemSafety] C++ and Pointers
>
> Peter,
>
> > Tools like CodeSonar and Astree can handle pointers and calculate the
> > set of pointer values for individual code paths, but because the
> > analysis is path-dependent it can take many hours, or even days to do a
> > complete analysis.
>
> Tools using late 90's algorithms are going to be slow.
>
> This is very recent, and the latest improvement this decade:
> https://yuleisui.github.io/publications/tse18.pdf
>
>
>
> > Peter
> >
> >>
> >> My company wrote the initial C t IL converter for the MALPAS tool,
> >> which was figuring this stuff out in the late 1980s.
> >>
> >>> Regards
> >>>
> >>> Peter
> >>>
> >>> On 05/07/2019 08:59, Grazebrook, Alvery AN wrote:
> >>>> Entertaining, but clearly a mis-quote out of context. Derek was
> >>>> making some (valid) comments about measuring the characteristics of
> >>>> buffer-overflow attacks, and then finished with:
> >>>> " I cannot think of any research looking at this.  Pointers welcome."
> >>>>
> >>>> Clearly not the endorsement of C++ programming that Olwen is
> >>>> accusing him of.
> >>>>
> >>>> Good opportunistic rant though!
> >>>>
> >>>> Cheers,
> >>>>      Alvery
> >>>>
> >>>> ** opinions are my own, not necessarily those of my employer
> >>>>
> >>>> -----Original Message-----
> >>>> From: systemsafety
> >>>> [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On
> >>>> Behalf Of Olwen Morgan
> >>>> Sent: 04 July 2019 19:45
> >>>> To: systemsafety at lists.techfak.uni-bielefeld.de
> >>>> Subject: Re: [SystemSafety] C++ and Pointers
> >>>>
> >>>>
> >>>> On 06/06/2019 17:18, Derek M Jones wrote:
> >>>>
> >>>> <snip>
> >>>>
> >>>> Pointers welcome.
> >>>>
> >>>>
> >>>> <snip>
> >>>>
> >>>>
> >>>> No, pointers are *unwelcome* owing to the complexity of aliasing and
> >>>> overflow problems they create. You can create efficient and secure
> >>>> large-scale services very easily with applicative/concurrent
> >>>> languages like Erlang.
> >>>>
> >>>> Software engineers who write critical systems in C++ should be sent
> >>>> to gulags to do more useful work.
> >>>>
> >>>>
> >>>> How long does one have to keep on saying these things before the
> >>>> lumpen-engineeriate finally gets it?
> >>>>
> >>>> Yawn,
> >>>>
> >>>> Olwen
> >>>>
> >>>>
> >>>> _______________________________________________
> >>>> The System Safety Mailing List
> >>>> systemsafety at TechFak.Uni-Bielefeld.DE
> >>>> Manage your subscription:
> >>>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> >>>> This email and its attachments may contain confidential and/or
> >>>> privileged information.  If you have received them in error you must
> >>>> not use, copy or disclose their content to any person.  Please
> >>>> notify the sender immediately and then delete this email from your
> >>>> system.  This e-mail has been scanned for viruses, but it is the
> >>>> responsibility of the recipient to conduct their own security
> >>>> measures. Airbus Operations Limited is not liable for any loss or
> >>>> damage arising from the receipt or use of this e-mail.
> >>>>
> >>>> Airbus Operations Limited, a company registered in England and
> >>>> Wales, registration number, 3468788.  Registered office:  Pegasus
> >>>> House, Aerospace Avenue, Filton, Bristol, BS34 7PA, UK.
> >>>>
> >>>> _______________________________________________
> >>>> The System Safety Mailing List
> >>>> systemsafety at TechFak.Uni-Bielefeld.DE
> >>>> Manage your subscription:
> >>>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> >>>
> >>
>
> --
> Derek M. Jones           Software analysis
> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: 
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety