CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Progress-sensitive security for SPARK

W. Rafnsson ; D. Garg ; Andrei Sabelfeld (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science: 8th International Symposium on Engineering Secure Software and Systems, ESSoS 2016, London, United Kingdom, 6-8 April 2016 (0302-9743). Vol. 9639 (2016), p. 20-37.
[Konferensbidrag, refereegranskat]

SPARK 2014 is a safety critical language subset of Ada developed by Altran and used for developing safe and secure software by major industrial players in the aviation, commercial, medical, space, and military domains. This paper puts a spotlight on the SPARK flow analysis. Articulating the boundaries of what is achievable by the analysis, we spell out attacks to exploit termination, progress, resource exhaustion, and timing channels. We harden the analysis to achieve security against stronger attackers, with the focus on progress-sensitive security as our baseline. Instead of redesigning and reimplementing the enforcement, we leverage known flow analyses for weaker attackers by a transform on program dependence graphs. We establish the soundness of this approach for a core language and demonstrate that it can be applied as a source-to-source transform of SPARK code when modifying the compiler is undesirable. A case study, derived from publicly available code for a control unit of a missile, indicates the usefulness of the approach.



Denna post skapades 2016-05-11. Senast ändrad 2016-06-27.
CPL Pubid: 236239

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Programvaruteknik

Chalmers infrastruktur