Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
An algebraic framework for reasoning about security
Thesis (MSc)--Stellenbosch University, 2013.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2013
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613902332755968 |
|---|---|
| access_status_str | Open Access |
| author | Rajaona, Solofomampionona Fortunat |
| author2 | Sanders, J. W. |
| author_browse | Rajaona, Solofomampionona Fortunat Sanders, J. W. |
| author_facet | Sanders, J. W. Rajaona, Solofomampionona Fortunat |
| author_sort | Rajaona, Solofomampionona Fortunat |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (MSc)--Stellenbosch University, 2013. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/79869 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:43:31.605Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2013 |
| publishDateRange | 2013 |
| publishDateSort | 2013 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/79869 An algebraic framework for reasoning about security Rajaona, Solofomampionona Fortunat Sanders, J. W. Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Shadow semantics Laws Security Completeness Dissertations -- Mathematics Theses -- Mathematics Computer software -- Development Computer software -- Verification 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. 2013-02-21T13:17:25Z 2013-03-15T07:24:27Z 2013-02-21T13:17:25Z 2013-03-15T07:24:27Z 2013-03 Thesis http://hdl.handle.net/10019/9983 http://hdl.handle.net/10019.1/79869 en_ZA Stellenbosch University 56 p. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Shadow semantics Laws Security Completeness Dissertations -- Mathematics Theses -- Mathematics Computer software -- Development Computer software -- Verification Rajaona, Solofomampionona Fortunat An algebraic framework for reasoning about security |
| title | An algebraic framework for reasoning about security |
| title_full | An algebraic framework for reasoning about security |
| title_fullStr | An algebraic framework for reasoning about security |
| title_full_unstemmed | An algebraic framework for reasoning about security |
| title_short | An algebraic framework for reasoning about security |
| title_sort | algebraic framework for reasoning about security |
| topic | Shadow semantics Laws Security Completeness Dissertations -- Mathematics Theses -- Mathematics Computer software -- Development Computer software -- Verification |
| url | http://hdl.handle.net/10019/9983 http://hdl.handle.net/10019.1/79869 |
| work_keys_str_mv | AT rajaonasolofomampiononafortunat analgebraicframeworkforreasoningaboutsecurity AT rajaonasolofomampiononafortunat algebraicframeworkforreasoningaboutsecurity |