• norsk
    • English
  • English 
    • norsk
    • English
  • Login
View Item 
  •   Home
  • Fakultet for informasjonsteknologi og elektroteknikk (IE)
  • Institutt for informasjonssikkerhet og kommunikasjonsteknologi
  • View Item
  •   Home
  • Fakultet for informasjonsteknologi og elektroteknikk (IE)
  • Institutt for informasjonssikkerhet og kommunikasjonsteknologi
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Specification of security properties by JML

Dulaj, Ilir
Master thesis
Thumbnail
View/Open
353056_FULLTEXT01.pdf (2.156Mb)
353056_COVER01.pdf (47.99Kb)
353056_ATTACHMENT01.zip (68.18Kb)
URI
http://hdl.handle.net/11250/262311
Date
2010
Metadata
Show full item record
Collections
  • Institutt for informasjonssikkerhet og kommunikasjonsteknologi [2775]
Abstract
Nowadays, verification of programs is gaining increased importance. The software industry appears more and more interested in methods and tools to ensure security in their applications. Java Modeling Language has been successfully used in the past by programmers to express their intentions in the Design by Contract fashion in sequential programming. One of the design goals of JML was to improve the functional software correctness of Java applications. Regarding the verification of security properties, JML was mostly successful in Java Smart Card applets due to the specifics of these applications. In this thesis work we investigate the feasibility of JML to express high-level security properties in Java applications that have more realistic requirements and are implemented in the object oriented technology. We do a threat analysis of a case study regarding a medical clinic and derive the required security properties to secure the application. We develop a prototype application where we specify high-level security properties with JML and use a runtime assertion checking tool to verify the code. We model the functional behavior of the prototype that establishes the security proper-ties as a finite state automaton. Our prototype is developed based on this automaton. States and state transitions modeled in the automaton are expressed in the prototype with JML annotations and verified during runtime. We observe that currently available features in JML are not very feasible to capture the security related behavior of Java programs on the level of the entire application.
Publisher
Institutt for telematikk

Contact Us | Send Feedback

Privacy policy
DSpace software copyright © 2002-2019  DuraSpace

Service from  Unit
 

 

Browse

ArchiveCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsDocument TypesJournalsThis CollectionBy Issue DateAuthorsTitlesSubjectsDocument TypesJournals

My Account

Login

Statistics

View Usage Statistics

Contact Us | Send Feedback

Privacy policy
DSpace software copyright © 2002-2019  DuraSpace

Service from  Unit