Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: Stepwise development of a program using refinement ensures that the program
correctly implements its requirements. The specification of a system is
“refined” incrementally to derive an implementable program. The programming
space includes both specifications and implementable code, and is ordered with
the refinement relation which obeys some mathematical laws. Morgan proposed a
modification of this “classical” refinement for systems where the confidentiality of
some information is critical. Programs distinguish between “hidden” and “visible”
variables and refinement has to bear some security requirement. First, we review
refinement for classical programs and present Morgan’s approach for ignorance pre-
serving refinement. We introduce the Shadow Semantics, a programming model
that captures essential properties of classical refinement while preserving the ignorance
of hidden variables. The model invalidates some classical laws which do
not preserve security while it satisfies new laws. Our approach will be algebraic,
we propose algebraic laws to describe the properties of ignorance preserving refinement.
Thus completing the laws proposed in. Moreover, we show
that the laws are sound in the Shadow Semantics. Finally, following the approach of Hoare and He for classical programs, we give a completeness result for the
program algebra of ignorance preserving refinement. / AFRIKAANSE OPSOMMING: Stapsgewyse ontwikkeling van ’n program met behulp van verfyning verseker dat
die program voldoen aan die vereistes. Die spesifikasie van ’n stelsel word geleidelik
”verfyn” wat lei tot ’n implementeerbare kode, en word georden met ‘n
verfyningsverhouding wat wiskundige wette gehoorsaam. Morgan stel ’n wysiging
van hierdie klassieke verfyning voor vir stelsels waar die vertroulikheid van
sekere inligting van kritieke belang is. Programme onderskei tussen ”verborgeën
”sigbare” veranderlikes en verfyning voldoen aan ’n paar sekuriteitsvereistes. Eers
hersien ons verfyning vir klassieke programme en verduidelik Morgan se benadering
tot onwetendheid behoud. Ons verduidelik die ”Shadow Semantics”, ’n programmeringsmodel
wat die noodsaaklike eienskappe van klassieke verfyning omskryf
terwyl dit die onwetendheid van verborge veranderlikes laat behoue bly. Die model
voldoen nie aan n paar klassieke wette, wat nie sekuriteit laat behoue bly nie,
en dit voldoen aan nuwe wette. Ons benadering sal algebraïese wees. Ons stel
algebraïese wette voor om die eienskappe van onwetendheid behoudende verfyning
te beskryf, wat dus die wette voorgestel in voltooi. Verder wys ons dat die wette konsekwent is in die ”Shadow Semantics”. Ten slotte, na aanleiding
van die benadering in vir klassieke programme, gee ons ’n volledigheidsresultaat
vir die program algebra van onwetendheid behoudende verfyning.
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:sun/oai:scholar.sun.ac.za:10019.1/79869 |
| Date | 03 1900 |
| Creators | Rajaona, Solofomampionona Fortunat |
| Contributors | Sanders, J. W., Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. |
| Publisher | Stellenbosch : Stellenbosch University |
| Source Sets | South African National ETD Portal |
| Language | en_ZA |
| Detected Language | English |
| Type | Thesis |
| Format | 56 p. |
| Rights | Stellenbosch University |
Page generated in 0.002 seconds