Astrée (statická analýza) - Astrée (static analysis) - Wikipedia
Astrée ("Analyseur statique de logiciels temps-reel Embarqués "[1]) je statický analyzátor na základě abstraktní interpretace. Analyzuje programy napsané v programovací jazyk C. a vydává vyčerpávající seznam možných chyb za běhu a tvrzení porušení. Pokryté třídy závad zahrnují dělení nulou, přetečení vyrovnávací paměti, dereference nula nebo visící ukazatele, datové závody, zablokování atd. Astrée obsahuje statickou elektřinu kontrola pachu a pomáhá najít zranitelnosti kybernetické bezpečnosti, jako Přízrak.
Nástroj je šitý na míru bezpečnostně důležitému vestavěnému kódu: běžné analytické techniky se běžně používají teorie řízení konstrukty (konečné stavové automaty, digitální filtry, omezovače sazeb ...) a plovoucí bod čísla.
Souběžný kód je analyzován sémantikou zvukového prokládání, která si je vědoma souběžnosti vlákna exekuce, jejich priority a synchronizační mechanismy. Astrée podporuje ARINC 653, OSEK a AUTOSAR modely provedení a lze je přizpůsobit dalším specifikacím OS. Na vícejádrové procesory umístění vláken na jádra a použití zámky mutex a spinlocky jsou brány v úvahu.
Astrée byla vyvinuta v Patrick Cousot je skupina v École Normale Supérieure, společná skupina s CNRS, a je prodáván společností AbsInt GmbH. Používá se v obranném / leteckém a kosmickém průmyslu, průmyslovém řízení, elektronickém a automobilovém průmyslu. Jedním z hlavních průmyslových uživatelů je Airbus.[2]
Astrée je komerční produkt dostupný od AbsInt Angewandte Informatik.
Viz také
Bibliografie
- Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux a Xavier Rival. Návrh a implementace speciálního statického programového analyzátoru pro bezpečnostní kritický software v reálném čase, pozvaná kapitola. v Podstata výpočtu: složitost, analýza, transformace. Eseje věnované Neilovi D. Jonesovi, T. Mogensen a D.A. Schmidt a I.H. Sudborough (redaktoři). Svazek 2566 přednášek z informatiky, str. 85–108, Springer. doi:10.1007/3-540-36377-7_5
- Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux a Xavier Rival, Statický analyzátor pro velký bezpečnostní software.„In PLDI 2003 - ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, 2003 Federated Computing Research Conference, 7. června - 14. června 2003, San Diego, Kalifornie, USA, str. 196–207, ACM. doi:10.1145/781131.781153
- David Delmas a Jean Souyris. Astrée: od výzkumu po průmysl., Proc. 14th International Static Analysis Symposium, SAS 2007, G. Filé & H. Riis-Nielson (eds), Kongens Lyngby, Denmark, 22. – 24. Srpna 2007, LNCS 4634, str. 437–451
- Arnaud J. Venet a Michael R. Lowry. 2010. Statická analýza pro zajištění softwaru: spolehlivost, škálovatelnost a přizpůsobivost. In Proceedings of the FSE / SDP workshop on Future of software engineering research (FoSER '10). ACM, New York, NY, USA, 393-396. doi:10.1145/1882362.1882442
- Jean-Louis Boulanger. Statická analýza softwaru: abstraktní interpretace. ISBN 978-1-84821-320-3. Wiley.
- Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival. Astrée: Prokazování nepřítomnosti běhových chyb. Embedded Real Time Software and Systems Congress ERTS², Toulouse, 2010.
- A. Miné, L. Mauborgne, X. Rival, J. Feret, P. Cousot, D. Kästner, S. Wilhelm, C. Ferdinand. Posunutí statické analýzy na další úroveň: Prokázání absence chyb za běhu a datových závodů s Astrée. V rámci ERTS 2016: Embedded Real Time Software and Systems, 8. evropský kongres, leden 2016, Toulouse, Francie.
- D. Kästner, L. Mauborgne, N. Grafe, C. Ferdinand. Pokročilá statická analýza zvuku k detekci bezpečnostních a bezpečnostně významných vad programování. 8. mezinárodní věstník o pokroku v oblasti bezpečnosti, ISSN 1942-2636, sv. 11, č. 1 & 2, 149-159, IARIA, 2018.
- D. Kästner, B. Schmidt, M. Schlundt, L. Mauborgne, S. Wilhelm, C. Ferdinand. Analyzujte to! Zvuková statická analýza pro ověření integrace rozsáhlého automobilového softwaru. SAE Technical Paper 2019-01-1246, SAE World Congress 2019, Detroit, duben 2019. doi:10.4271/2019-01-1246