SIFA: A tool for evaluation of high-grade security devices

We describe a tool for analysing information flow in security hardware. It identifies both sub-circuits critical to the preservation of security as well as the potential for information flow due to hardware failure. The tool allows for the composition of both logical and physical views of circuit designs. An example based on a cryptographic device is provided.

A software audit framework for spyware risk mitigation

Our research described in this paper identifies a three part premise relating to the spyware paradigm. Firstly the data suggests spyware is proliferating at an exponential rate. Secondly ongoing research confirms that spyware produces many security risks – including that of privacy/confidentiality breaches via illicit data collection and reporting. Thirdly, anti-spyware controls are improving but are still considered problematic for several reasons. Our research then concludes that control measures to counter this very significant challenge should merit compliance auditing – and this auditing may effectively target the vital message passing performed by all illicit data collection spyware. Our research then evolves into an experiment involving the design and implementation of a software audit tool to conduct the desired compliance auditing. The software audit tool is positioned at the protected network’s gateway. The software audit tool uses ‘phone-home’ IP addresses as spyware signatures to detect the presence of the offending software. The audit tool also has the capability to differentiate legitimate message passing software from that produced by spyware – and ‘learn’ both new spyware signatures and new legitimate message passing profiles. The testing stage of the software has proven successful – albeit using very limited levels of network message passing variety and frequency.

Verifying abstract information flow properties in fault tolerant security devices

The verification of information flow properties of security devices is difficult because it involves the analysis of schematic diagrams, artwork, embedded software, etc. In addition, a typical security device has many modes, partial information flow, and needs to be fault tolerant. We propose a new approach to the verification of such devices based upon checking abstract information flow properties expressed as graphs. This approach has been implemented in software, and successfully used to find possible paths of information flow through security devices.

A Z based approach to verifying security protocols

Security protocols preserve essential properties, such as confidentiality and authentication, of electronically transmitted data. However, such properties cannot be directly expressed or verified in contemporary formal methods. Via a detailed example, we describe the phases needed to formalise and verify the correctness of a security protocol in the state-oriented Z formalism.

Formal verification of type flaw attacks in security protocols

Security protocols are often modelled at a high level of abstraction, potentially overlooking implementation-dependent vulnerabilities. Here we use the Z specification language's rich set of data structures to formally model potentially ambiguous messages that may be exploited in a 'type flaw' attack. We then show how to formally verify whether or not such an attack is actually possible in a particular protocol using Z's schema calculus.

Articulating wider smartphone emerging security issues in the case of M-government in Turkey

For the last several years, mobile devices and platform security threats, including wireless networking technology, have been top security issues. A departure has occurred from automatic anti-virus software based on traditional PC defense: risk management (authentication and encryption), compliance, and disaster recovery following polymorphic viruses and malware as the primary activities within many organizations and government services alike. This chapter covers research in Turkey as a reflection of the current market – e-government started officially in 2008. This situation in an emerging country presents the current situation and resistances encountered while engaging with mobile and e-government interfaces. The authors contend that research is needed to understand more precisely security threats and most of all potential solutions for sustainable future intention to use m-government services. Finally, beyond m-government initiatives' success or failure, the mechanisms related to public administration mobile technical capacity building and security issues are discussed.

Integrating security services into computer supported cooperative work

This research describes the development of a groupware system which adds security services to a Computer Supported Cooperative Work system operating over the Internet. The security services use cryptographic techniques to provide a secure access control service and an information protection service. These security services are implemented as a protection layer for the groupware system. These layers are called External Security Layer (ESL) and Internal Security Layer (ISL) respectively. The security services are sufficiently flexible to allow the groupware system to operate in both synchronous and asynchronous modes. The groupware system developed - known as Secure Software Inspection Groupware (SecureSIG) - provides security for a distributed group performing software inspection. SecureSIG extends previous work on developing flexible software inspection groupware (FlexSIG) Sahibuddin, 1999). The SecureSIG model extends the FlexSIG model, and the prototype system was added to the FlexSIG prototype. The prototype was built by integrating existing software, communication and cryptography tools and technology. Java Cryptography Extension (JCE) and Internet technology were used to build the prototype. To test the suitability and transparency of the system, an evaluation was conducted. A questionnaire was used to assess user acceptability.

Refinement methods for software architecture design using the software architecture model

Modern software systems are often large and complicated. To better understand, develop, and manage large software systems, researchers have studied software architectures that provide the top level overall structural design of software systems for the last decade. One major research focus on software architectures is formal architecture description languages, but most existing research focuses primarily on the descriptive capability and puts less emphasis on software architecture design methods and formal analysis techniques, which are necessary to develop correct software architecture design. ^ Refinement is a general approach of adding details to a software design. A formal refinement method can further ensure certain design properties. This dissertation proposes refinement methods, including a set of formal refinement patterns and complementary verification techniques, for software architecture design using Software Architecture Model (SAM), which was developed at Florida International University. First, a general guideline for software architecture design in SAM is proposed. Second, specification construction through property-preserving refinement patterns is discussed. The refinement patterns are categorized into connector refinement, component refinement and high-level Petri nets refinement. These three levels of refinement patterns are applicable to overall system interaction, architectural components, and underlying formal language, respectively. Third, verification after modeling as a complementary technique to specification refinement is discussed. Two formal verification tools, the Stanford Temporal Prover (STeP) and the Simple Promela Interpreter (SPIN), are adopted into SAM to develop the initial models. Fourth, formalization and refinement of security issues are studied. A method for security enforcement in SAM is proposed. The Role-Based Access Control model is formalized using predicate transition nets and Z notation. The patterns of enforcing access control and auditing are proposed. Finally, modeling and refining a life insurance system is used to demonstrate how to apply the refinement patterns for software architecture design using SAM and how to integrate the access control model. ^ The results of this dissertation demonstrate that a refinement method is an effective way to develop a high assurance system. The method developed in this dissertation extends existing work on modeling software architectures using SAM and makes SAM a more usable and valuable formal tool for software architecture design. ^

Analisi di aspetti di Security da attacchi informatici su Impianti di Processo

Gli impianti industriali moderni sono di tipo automatizzato, i processi sono cioè pilotati da un’unità di calcolo che fornisce i comandi necessari atti al corretto funzionamento dell’impianto. Queste tecnologie espongono le apparecchiature a problemi di Security, dunque attacchi volontari provenienti dall’esterno, al sistema di controllo. Esso può diventare la variabile manipolabile del terrorista informatico il quale può causare lo shut down del segnale o cambiare l’impostazione dei parametri di processo.Lo studio esposto si propone di identificare le possibili modalità di attacco e di individuare uno strumento sistematico che permetta di valutarne la vulnerabilità ad un possibile atto di sabotaggio. La procedura proposta è la PSC-SHaRP (Process System Cyber-Security Hazard Review Procedure) essa consta di due strutture chiamate rispettivamente Alpha e Beta. La metodologia è volta a individuare i potenziali pericoli posti dagli attacchi informatici piuttosto che a stimarne un profilo di rischio e/o probabilità di successo. La ShaRP Alpha, viene utilizzata per analizzare le conseguenze di deviazioni cyber su singole macchine presenti in impianto o sistemi modulari. La ShaRP Beta viene utilizzata per analizzare le conseguenze di attacchi cyber sul sistema costituito dall’impianto di processo. Essa è quindi in grado di analizzare le ripercussioni che manipolazioni su una o più apparecchiature possono avere sull’impianto nel suo complesso. Nell’ultima parte dell’elaborato sono state trattate le possibilità di accesso da parte del ‘’terrorista’’ al sistema di controllo e sicurezza, dunque i sistemi di gestione del DCS e del SIS e le barriere software e hardware che possono essere presenti.

Attack simulation based software protection assessment method

Software protection is an essential aspect of information security to withstand malicious activities on software, and preserving software assets. However, software developers still lacks a methodology for the assessment of the deployed protections. To solve these issues, we present a novel attack simulation based software protection assessment method to assess and compare various protection solutions. Our solution relies on Petri Nets to specify and visualize attack models, and we developed a Monte Carlo based approach to simulate attacking processes and to deal with uncertainty. Then, based on this simulation and estimation, a novel protection comparison model is proposed to compare different protection solutions. Lastly, our attack simulation based software protection assessment method is presented. We illustrate our method by means of a software protection assessment process to demonstrate that our approach can provide a suitable software protection assessment for developers and software companies.

Early investigation towards defining and measuring sustainability as a quality attribute in software systems

Sustainability in software system is still a new practice that most software developers and companies are trying to incorporate into their software development lifecycle and has been largely discussed in academia. Sustainability is a complex concept viewed from economic, environment and social dimensions with several definitions proposed making sometimes the concept of sustainability very fuzzy and difficult to apply and assess in software systems. This has hindered the adoption of sustainability in the software industry. A little research explores sustainability as a quality property of software products and services to answer questions such as; How to quantify sustainability as a quality construct in the same way as other quality attributes such as security, usability and reliability? How can it be applied to software systems? What are the measures and measurement scale of sustainability? The Goal of this research is to investigate the definitions, perceptions and measurement of sustainability from the quality perspective. Grounded in the general theory of software measurement, the aim is to develop a method that decomposes sustainability in factors, criteria and metrics. The Result is a method to quantify and access sustainability of software systems while incorporating management and users concern. Conclusion: The method will empower the ability of companies to easily adopt sustainability while facilitating its integration to the software development process and tools. It will also help companies to measure sustainability of their software products from economic, environmental, social, individual and technological dimension.

A HUMAN-CENTERED APPROACH TO IMPROVING THE USER EXPERIENCE OF SOFTWARE UPDATES

Software updates are critical to the security of software systems and devices. Yet users often do not install them in a timely manner, leaving their devices open to security exploits. This research explored a re-design of automatic software updates on desktop and mobile devices to improve the uptake of updates through three studies. First using interviews, we studied users’ updating patterns and behaviors on desktop machines in a formative study. Second, we distilled these findings into the design of a low-fi prototype for desktops, and evaluated its efficacy for automating updates by means of a think-aloud study. Third, we investigated individual differences in update automation on Android devices using a large scale survey, and interviews. In this thesis, I present the findings of all three studies and provide evidence for how automatic updates can be better appropriated to fit users on both desktops and mobile devices. Additionally, I provide user interface design suggestions for software updates and outline recommendations for future work to improve the user experience of software updates.