Most existing work to thwart malicious web pages capture maliciousness via discriminative artifacts, learn a model, and detect by leveraging static and/or dynamic analysis. Unfortunately, there is a two-sided evolution of the artifacts of web pages. On one hand, cybercriminals constantly revamp attack payloads in malicious web pages. On the other hand, benign web pages evolve to improve content rendering and interaction with users. Consequently, the once precise detection techniques suffer from limitations to cope with the evolution, resulting in malicious web pages that escape detection. In this paper, we present EINSPECT, an evolution-aware and learning-based approach to address evolution of web page artifacts to more robustly analyze and detect malicious web pages. EINSPECT continuously tunes its detection models to automatically decide the best interplay of features and learning algorithms to embrace the evolution of web page artifacts into the analysis and detection. We have implemented and evaluated our approach and the results show that EINSPECT is able to improve the effectiveness of analysis and detection of malicious web pages while aligning the detection models with the continuous evolution of web page artifacts.

Vulnerable web browser extensions can be used by an attacker to steal users’ credentials and lure users into leaking sensitive information to unauthorized parties. Current browser security models and existing JavaScript security solutions are inadequate for preventing JavaScript injection attacks that can exploit such vulnerable extensions. In this paper, we present a runtime protection mechanism based on code randomization technique coupled with a static analysis technique to protect browser extensions from JavaScript injection attacks. The protection is enforced at runtime by distinguishing malicious code from the randomized extension code. We implemented our protection mechanism for Mozilla Firefox browser and evaluated it on a set of vulnerable and non-vulnerable Firefox extensions. The evaluation results indicate that our approach can be a viable solution for preventing attacks on JavaScript-based browser extensions. In designing and implementing our approach, we were also able to reduce false positives and achieve maximum backward compatibility with existing extensions by relieving developers from the burden of rewriting their extensions.

Distributed server environments and web applications rely on server-level and application-level configurations. These configurations influence the security, usability, and performance of the environment and applications deployed on it. Misconfiguration results in severe security vulnerabilities. The current trend also shows that security misconfiguration is among the top critical risks in web applications. While effective at uncovering numerous classes of vulnerabilities, generic web application vulnerability scanners are limited in identifying configuration vulnerability in practice. In this paper, we present an approach that effectively combines hierarchical configuration scanning and preliminary source code analysis of web applications to pinpoint potential configuration vulnerabilities, quantify the degree of severity based on standard metrics, and facilitate fixing of vulnerabilities found therein. We implemented our approach in a tool called Confeagle and evaluated it on 14 widely deployed PHP web applications. Unlike generic web vulnerability scanners, on the same set of subject applications, Confeagle is able to identify critical security configuration vulnerabilities. The detected vulnerabilities could have at least resulted in information disclosure, denial-of-service, and session hijacking attacks on the applications.

Browser extensions have become an integral part of Web browsers to enrich a browser with various functionalities. Unfortunately, they are frequently targeted by attackers. Attacks such as XSS and SQL injections are still common in browser extensions due to the presence of potential vulnerabilities in extensions and some extensions are also malicious by design. As a consequence, much effort in the past has been spent on detecting vulnerable and malicious browser extensions. These techniques are limited to only detect either new forms of vulnerable or malicious extensions but not both. In this paper, we present a model-based approach to detect vulnerable and malicious browser extensions by widening and complementing existing techniques. We observe and utilize various common and distinguishing characteristics of benign, vulnerable, and malicious extensions to build our detection models. The models are well trained using a set of features extracted from a number of widely used browser extensions together with user supplied specifications. We implemented the approach for Mozilla Firefox extensions and evaluated it in a number of browser extensions. Our evaluation indicates that the approach not only detects known vulnerable and malicious extensions, but also identifies previously undetected extensions with a negligible performance overhead.

Software defects data provide an invaluable source of information for developers, testers and so forth. A concise view of a software profile, its development process, and their relationships can be systematically extracted and analyzed to deduce adequate corrective measures based on previously discovered weaknesses. This kind of approach is being widely used in various projects to improve the quality of a software system. This paper builds on top of the orthogonal defect classification (ODC) scheme to provide a structured security-specific defects classification. We perform a detailed analysis on the classified data and obtain in-process feedback so that the next version of the software can be more secure and reliable. We experimented our customized methodology on Mozilla Firefox and Chrome defect repositories using six consecutive versions and milestones, respectively. We find that in-process feedback can help development team to take corrective actions as early as possible in secure software development process. Finally, we study the correlations between software defect types and software development lifecycle to understand development improvement, by complementing with the ODC scheme.

This paper presents a framework for ranking components by utilizing types of failures and pre-defined ranking features. The ultimate goal is that such a framework can help system developers in prioritizing components systematically for achieving a more reliable software system.

This paper presents our experience with the organization of the Summer School of ICTs (SSICT) of Maputo Living Lab. SSICT is a free 1-month course for 3rd and 4th year undergraduate students that provides practical training on the management, design and development of software projects that can have an impact on the local society. The School has been organized for 2 editions in 2011 and 2012 in Maputo, Mozambique and it is part of the larger Maputo Living Lab project.

Malicious web pages are among the major security threats on the Web. Most of the existing techniques for detecting malicious web pages focus on specific attacks. Unfortunately, attacks are getting more complex whereby attackers use blended techniques to evade existing countermeasures. In this paper, we present a holistic and at the same time lightweight approach, called BINSPECT, that leverages a combination of static analysis and minimalistic emulation to apply supervised learning techniques in detecting malicious web pages pertinent to drive-by-download, phishing, injection, and malware distribution by introducing new features that can effectively discriminate malicious and benign web pages. Large scale experimental evaluation of BINSPECT achieved above 97% accuracy with low false signals. Moreover, the performance overhead of BINSPECT is in the range 3-5 seconds to analyze a single web page, suggesting the effectiveness of our approach for real-life deployment.

During past few years a huge interests in e-voting has occurred, which resulted in a significant funding for e- voting research and development (R&D) projects, with the aim of developing trustworthy e-voting systems. Although it is good that major e-voting development trends are capitalizing on previous R&D efforts in other domains, it is difficult to say that the necessary R&D efforts has been utilized to realize the vision and principles of e-voting. Today, we now have a much better understanding of the issues that pose the development of a trustworthy e-voting system. In this paper, we categorize and analyze the most important research and development trends in e-voting systems. We identify the lessons learned from these projects and analyze whether the existing R&D projects meet the identified flaws in past. Finally, based on these results the way to the future of e-voting R&D is postulated.

Vote verification allows voters or other election participating entities to verify that votes are correctly captured, stored and counted. To facilitate the vote verification process, a number of verification techniques (either physical or digital) have developed that provide a sort of evidence to voters and other participating entities for the assurance of the integrity of election result. However, we observed that these techniques have a number of limitations among which: the existing techniques do not fully comply with verification requirements (e.g., the public verifiability); they implement limited prevention mechanism from known attacks; they are not based on interoperable components and processes (typically, vendor lock-in). In order to address these issues, we propose a new method for vote verification based on open standards which allows interested party or organization to participate in a vote verification process so as to enhance transparency and capture vote threats and challenges during and after elections. Our proposed vote verification method is for e-voting system.

Many studies into the diffusion of business innovation in the information systems for agriculture (IS4A) focused on factors associated with the act of adopting ICT for agriculture. In this paper we present the result of a study that identifies the limitations of existing IS4A with respect to service coverage, rural accessibility, delivery channels, open standards, and long-term sustainability among others. We then present a road-map for the development of IS4A that includes the identification of relevant stakeholders in agricultural sector, their roles and requirements for IS4A. Lastly, we propose an architecture for a distributed service delivery with the aim of achieving a platform with qualifying characteristics such as aggregated services and multi-channel service delivery based on ICTD best practices and open standards.

This paper presents a web-based tool to supplement defense against security misconfiguration vulnerabilities in web applications. The tool automatically audits security con- figuration settings of server environments in web application development and deployment. It also offers features to automatically adjust security configuration settings and quantitatively rates level of safety for server environments before deploying web applications. Using the tool, we were able to evaluate eleven server packages for Apache, PHP and MySQL across three operating system platforms. Our evaluation revealed that the tool is able to audit current security configuration settings and alert users to fix the server environment to achieve the level of safety of security configuration with respect to recommended configurations for real-life web application deployment.

Modeling and analysis of legal documents is becoming more widely used in eGovernment practices. To support these activities, various frameworks, standards, and ICT-based tools have been developed in the recent years. These approaches are mostly oriented towards defining common standards, managing legal documents and check compliance with current regulations. Along this line, we have devised a tool-supported methodology that allows to model and analyze laws and procedures within public administrations. The approach used in this paper is based on BPMN for the visualization and formalization of business processes and on OWL-DL for the specification of a business process ontology. In this paper we demonstrate the applicability of our approach by using the part of the Italian Immigration Law concerning Family Reunification as a case study. From this initial investigation, our approach can be used on actual laws that describe or affect procedures.

Modeling and analysis of legal documents is becoming more widely used in eGovernment practices. To support these activities, various frameworks, standards, and ICT-based tools have been developed in the recent years. These approaches are mostly oriented towards defining common standards, managing legal documents and check compliance with current regulations. Along this line, we have devised a tool-supported methodology that allows to model and analyze laws and procedures within public administrations. The approach used in this paper is based on BPMN for the visualization and formalization of business processes and on OWL-DL for the specification of a business process ontology. In this paper we demonstrate the applicability of our approach by using the part of the Italian Immigration Law concerning Family Reunification as a case study. From this initial investigation, our approach can be used on actual laws that describe or affect procedures.

Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various e-voting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties. This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations.

Intrusion detection systems are deployed on hosts in a computing infrastructure to tackle undesired events in the course of usage of the systems. One of the promising domains of applying intrusion detection is the healthcare domain. A typical healthcare scenario is characterized by high degree of mobility, frequent interruptions and above all demands access to sensitive medical records by concerned stakeholders. Migrating this set of concerns in pervasive healthcare environments where the traditional characteristics are more intensified in terms of uncertainty, one ends up with more challenges on security due to nature of pervasive devices and wireless communication media along with classic security problems for desktop based systems. Despite evolution of automated healthcare services and sophistication of attacks against such services, there is a reasonable lack of techniques, tools and experimental setups for protecting hosts against intrusive actions. This paper presents a contribution to provide a host-based, anomaly modeling and detection approach based on data mining techniques for pervasive healthcare systems. The technique maintains normal usage profile of pervasive healthcare applications and inspects current workflow against normal usage profile so as to classify it as anomalous or normal. The technique is implemented as a prototype with sample data set and the results obtained revealed that the technique is able to perform classification of anomalous activities.

Any practitioner working on electronic voting (e-voting) seem to have stumbled upon the main issues that seem to affect the area. On the one hand - given the criticality and the risk e-voting systems potentially pose to the democratic process - e-voting systems are permanently under a magnifying glass that amplifies any glitch, be it significant or not. On the other hand, given the interest e-voting raises with the general public, there seems to be a tendency to generalize and oversimplify. This tendency leads to attribute specific problems to all systems, regardless of context, situation, and actual systems used. Additionally, scarce know-how about the electoral context often contributes to make matters even more confused. This is not to say all e-voting systems show the security and reliability characteristics that are necessary for system of such a criticality. On the contrary, a lot of work still has to be done. Starting from previous experiences and from a large-scale experimentation we conducted in Italy, this paper provides some directions, issues, and trends in e-voting. Getting a clearer view of the research activities in the area, highlighting both positive and negative results, and emphasizing some trends, could help, in our opinion, drawing a neater line between opinion from facts and contribute to the construction of a next generation of e-voting machines to be safely and more confidently employed for elections.

ICT seems well understood as a tool and an infrastructure for delivering information and services for the society and for allowing communications through interactions among the service users --mostly, the digital society. Using ICT for ensuring better life requires far more than good infrastructure, ICT know-how and the various techniques and tools in place. If ICT has to address the real problems of the society, it should be at a rescue being environment-friendly, with real and tangible impact, sustainable, seamless, down to the grass-roots and above all with reproducible experiences. In this paper, we introduce a different perspective of looking into and using ICT, which we call ICT for Good (ICT4G). It is about using ICT for addressing problems of societies with low ICT penetration and changing a society's life for the better. More specifically, based on our observation of current promises ICT gives to society, we discuss ICT4G's distinguishing aspects, opportunities it offers, challenges it imposes along with preliminary roadmap for its realization. A high-level correlation of what we pointed out with a relevant case study is presented.

Emerging technologies like mobile and wireless communication are offering promising opportunities to enable mobile healthcare delivery to citizens. But, enhancing the quality of service of such systems demands systematic improvement of existing service infrastructure. In this paper, we describe a context information refinement architecture proposed to address the shortcomings of existing works in relation to context information refinement in pervasive medical systems. The shortcomings are lack of adequate consideration for: quality parameters of context information, relevance of context information and particular requirements of the pervasive healthcare domain. The proposed architecture facilitates and coordinates the refinement of context information starting from acquisition of context information up until the refined context information is delivered to the target application in a pervasive medical system. We developed a prototype that implements the core components of the proposed architecture and evaluated it with real-life pervasive healthcare scenario and proved the validity of the architecture using a real-life scenario.

Electronic voting systems are a perfect example of security-critical computing. One of the critical and complex parts of such systems is the voting process, which is responsible for correctly and securely storing intentions and actions of the voters. Unfortunately, recent studies revealed that various e-voting systems show serious specification, design, and implementation flaws. The application of formal specification and verification can greatly help to better understand the system requirements of e-voting systems by thoroughly specifying and analyzing the underlying assumptions and the security specific properties. This paper presents the specification and verification of the electronic voting process for the Election Systems & Software (ES&S) system. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations.

Modeling and analysis of legal documents is becoming more widely used in eGovernment practices. To support these activities, various frameworks, standards, and ICT-based tools have been developed in the recent years. These approaches are mostly oriented towards defining common standards, managing legal documents and check compliance with current regulations. Along this line, we have devised a tool-supported methodology that allows to model and analyze laws and procedures within public administrations. The approach used in this paper is based on BPMN for the visualization and formalization of business processes and on OWL-DL for the specification of a business process ontology. In this paper we demonstrate the applicability of our approach by using the part of the Italian Immigration Law concerning Family Reunification as a case study. From this initial investigation, our approach can be used on actual laws that describe or affect procedures.

Recently, the use of formal methods to specify and verify properties of electronic voting (e-voting) systems, with particular interest in security, verifiability, and anonymity, is getting much attention. Formal specification and verification of such systems can greatly help to better understand the system requirements by thoroughly specifying and analyzing the underlying assumptions and security specific properties. Unfortunately, even though these systems have been formally verified to satisfy the desired system security requirements, they are still vulnerable to attack. In this paper we extend a formal specification of the ES&S voting system by specifying attacks that have been shown to successfully compromise the system. We believe that performing such analysis is important for two reasons: first, it allows us to discover some missing critical requirements for the specification and/or assumptions that were not met. Second, it allows us to derive mitigation or counter-measure strategies when the system behaves differently than it should. We used the ASTRAL language for the specification, and the verification is performed using the PVS tool.

Experimental data sets related to e-voting systems are very demanding in order to improve currently deployed e-voting machines. Unfortunately, the studies of such data about the machines' security, performance and their evolution with respect to the social and technical aspects are still unsatisfactory. During the last four years we have been involved in the development, experimentation, and evaluation of an e-voting system. The system tried out in several regular elections, and also used in two small elections with legal value. Each experiment provided various sociological (e.g. citizens' opinions on the system) and technical data that are related to system's performance and behavior. In this paper, we present various technical insights and the lessons learned during the e-voting experiment. The method- ology for the various experiments we have carried-out and the data sets collection process are also discussed. This helps to confirm existing data on the subject (e.g., data related to security, procedures and logistics) and, in some cases, provide novel information or, at least, shed a new perspective on some security-critical factors concerning e-voting systems.

The definition or redesign of Public Administration (PA) procedures is particularly challenging. This is, for example, due to the requirement of cooperation of different organizational units and actors, different laws and procedures for the production of several artifacts, and maintaining traceability while integrating processes with new laws. We are interested in business process modeling and re-engineering (BPR) for PA, where ICT can play a pivotal role by, e.g., improving communication among law-makers and process analysts. With regard to this previously we developed a tool called VLPM. The tool is designed to provide assistance in BPR for PA, which allows traceability between laws and processes. In this paper, we discuss the extension of the tool and of its methodology to support an integrated environment that can be used for better law and process re-design by performing formal analysis on the processes. We discuss its system components and provide a working example taken from the Italian Immigration law, as a proof of concept.

This paper presents a methodology for procedural security analysis in order to analyze and eventually try to make elections more secure. Our approach is based on modelling the electoral procedures in the form of business process models (which we write in a strict simplified subset of UML), systematically translate the models into executable formal specifications, and analyze the specifications against security properties. We believe such an analysis to be essential to identifying the limits of the current procedures (i.e., undetected attacks) and to identify more precisely under what hypotheses we can guarantee secure elections. This paper presents the approach and demonstrates with an example taken from the e-Voting procedures enacted within the ProVotE project, current trial of the Italian legislation.

This paper presents a methodology for procedural security analysis in order to analyze and eventually try to make elections more secure. Our approach is based on modelling the electoral procedures in the form of business process models (which we write in a strict simplified subset of UML), systematically translate the models into executable formal specifications, and analyze the specifications against security properties. We believe such an analysis to be essential to identifying the limits of the current procedures (i.e., undetected attacks) and to identify more precisely under what hypotheses we can guarantee secure elections. This paper presents the approach and demonstrates with an example taken from the e-Voting procedures enacted within the ProVotE project, current trial of the Italian legislation.

Performing a good security analysis on the design of asystem is an essential step in order to guarantee a reasonable level of protection. However, different attacks and threats may be carried out depending on the operational environment in which the system is used, i.e. the procedures that define how to operate the systems. We are interested in reasoning about the security of e-Voting procedures, namely on the risks and attacks that can be carried out during an election. Our focus is more on people and organizations than on systems and technologies. In this paper we describe some ongoing work that we are carrying out within the ProVotE project (a project sponsored by the Autonomous Province of Trento to switch to e-Voting for local elections) to analyze and (possibly) improve procedural security of electronic elections. To do so, we are providing models of the Italian electoral laws using the UML and we are developing a custom methodology for analyzing threats from the models. Our reasoning approach is based on asset mobility, asset values and existence of multiple instances.

Many studies into the diffusion of business innovation in the information systems for agriculture (IS4A) focused on factors associated with the act of adopting ICT for agriculture. In this paper we present the result of a study that identifies the limitations of existing IS4A with respect to service coverage, rural accessibility, delivery channels, open standards, and long-term sustainability among others. We then present a road-map for the development of IS4A that includes the identification of relevant stakeholders in agricultural sector, their roles and requirements for IS4A. Lastly, we propose an architecture for a distributed service delivery with the aim of achieving a platform with qualifying characteristics such as aggregated services and multi-channel service delivery based on ICTD best practices and open standards.

We have seen that several currently deployed e-voting systems share critical failures in their design and implementation that render their technical and procedural controls insufficient to guarantee trustworthy voting. The application of formal methods would greatly help to better address problems associated with assurance against requirements and standards. More specifically, it would help to thoroughly specify and analyze the underlying assumptions and security specific properties, and it would improve the trustworthiness of the final systems.

In this article, we show how such techniques can be used to model and reason about the security of one of the currently deployed e-voting systems in the U.S.A named ES&S. We used the ASTRAL language to specify the voting process of ES&S machines and the critical security requirements for the system. Proof obligations that verify that the specified system meets the critical requirements were automatically generated by the ASTRAL Software Development Environment (SDE). The PVS interactive theorem prover was then used to apply the appropriate proof strategies and discharge the proof obligations. We also believe that besides analyzing the system against its requirements, it is equally important to perform an analysis under malicious circumstances where the execution model is augmented with attack behaviors. Thus, we extend the formal specification of the system by specifying attacks that have been shown to successfully compromise the system, and we then repeat the formal verification. This is helpful in detecting missing requirements or unwarranted assumptions about the specification of the system. In addition, this allows one to sketch countermeasure strategies to be used when the system behaves differently than it should and to build confidence about the system under development. Finally, we acknowledge the main problem that arises in e-voting system specification and verification: modeling attacks is very difficult because the different types of attack often cut across the structure of the original behavior models, thus making (incremental or compositional) verification very difficult.

Malicious websites, when visited by an unsuspecting victim infect her machine to steal invaluable information, redirect her to malicious targets or compromise her system to mount future attacks. While the existing approaches have promising prospects in detecting malicious websites, there are still open issues in effectively and efficiently addressing: filtering of web pages from the wild, coverage of wide range of malicious characteristics to capture the big picture, continuous evolution of web page features, systematic combination of features, semantic implications of feature values on characterizing web pages, ease and cost of flexibility and scalability of analysis and detection techniques with respect to inevitable changes to the threat landscape. In this position paper, we highlight our ongoing efforts towards effective and efficient analysis and detection of malicious websites with a particular emphasis on broader feature space and attack-payloads, flexibility of techniques with changes in malicious characteristics and web pages and above all real-life usability of techniques in defending users against malicious websites.

As the technology for e-voting changes day by day along with an evolution of the regulatory environment, many questions emerge. One of these questions is how to allow voters or any third party to verify votes are correctly captured, stored and counted. This underlines the fact that an e-voting system is not only responsible for ensuring its technical and procedural security, but also must provide a mechanism by which voters can verify their votes during and after casting, and third party be able to verify the correctness and integrity of election results. The purpose of this paper is to review currently deployed vote verification methods, by discuss their weaknesses with the aim of proposing a more reliable and robust vote verification method.

Experimental data sets related to e-voting systems are very demanding in order to improve currently deployed e-voting machines. Unfortunately, the studies of such data about the machines' security, performance and their evolution with respect to the social and technical aspects are still unsatisfactory. During the last four years we have been involved in the development, experimentation, and evaluation of an e-voting system. The system tried out in several regular elections, and also used in two small elections with legal value. Each experiment provided various sociological (e.g. citizens' opinions on the system) and technical data that are related to system's performance and behavior. In this paper, we present various technical insights and the lessons learned during the e-voting experiment. The method- ology for the various experiments we have carried-out and the data sets collection process are also discussed. This helps to confirm existing data on the subject (e.g., data related to security, procedures and logistics) and, in some cases, provide novel information or, at least, shed a new perspective on some security-critical factors concerning e-voting systems.

This paper describes the experiences and the challenges we are facing within the ProVotE project, a four years project sponsored by the Autonomous Province of Trento that has the goal of switching to e-voting for local elections. One of the activities we are carrying out within ProVotE is the systematic analysis of the weaknesses and strengths of the procedures regulating local elections in Italy, in order to derive possible attacks and their effects. The approach we take is based on providing formal specifications of the procedures and using model checkers to help us analyze the effects of attacks. We believe such an analysis to be essential to identify the limits of the current procedures (i.e., under what hypotheses attacks are undetectable) and to identify more precisely under what hypotheses and conditions we can guarantee reasonably secure electronic elections. This paper presents the methodology and the techniques we are devising and experimenting with to tackle problem highlighted above.

This paper presents a method of building executable and interactive application interface prototypes from requirements. The specification of the requirements uses i* and Formal Tropos languages.

The Internet has become an indispensable global platform that glues together daily communication, sharing, trading, collaboration, and service delivery using software applications. This is a witness that our society is increasingly dependant on software applications. Internet users often store and manage critical information that can attract cyber-criminals who misuse web-based programs and the Internet to exploit vulnerabilities for illegitimate benefits (such as for underground economy, violating privacy, etc.). Malicious programs are taking an alarmingly significant share of web- based attacks to evade the Security, Privacy, and Trust (STP) of software applications, and hence end-users. As noted also in several security incidents, this situation has been amplified by recent technological developments such as cloud computing, pervasive computing, mobile devices, by making the distrusted Internet an integral component of software applications. As such, the traditional host-based approaches (e.g., antivirus, firewall) to securing a software application alone are no longer sufficient to address the STP issues of such emerging software applications. The STP issues must be addressed throughout the lifecycle of a software application, including its design, implementation, testing, and deployment. The principal challenge of existing approaches in developing STP-aware software is the lack of consideration, methods, and tools for addressing STP issues during the software development processes and runtime operations.

REVOTE2011 was targeted to identify best-practice for the engineering of electronic voting (e-voting) system requirements and business process models, and to improve the current specification and development of the e-voting system standards and accreditation (certification) and verification processes. Particular attention was given to the (formal) analysis of voting requirements documents (e.g., recommendations, standards and guidelines), including those that pre-date e-voting.

In this chapter, first we discuss the current trends in the usage of formal techniques in the development of e-voting system. We then present our experiences on their usage to specify and verify the behaviors of one of currently deployed e-voting systems using formal techniques and verification against a subset of critical security properties that the system should meet. We also specified attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what we called the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where we would use formal techniques to improve the current development of e-voting systems.

In this chapter, first we discuss the current trends in the usage of formal techniques in the development of e-voting system. We then present our experiences on their usage to specify and verify the behaviors of one of currently deployed e-voting systems using formal techniques and verification against a subset of critical security properties that the system should meet. We also specified attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what we called the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where we would use formal techniques to improve the current development of e-voting systems.

Deploying a system in a safe and secure manner requires ensuring the tech- nical and procedural levels of assurance also with respect to social and regulatory frameworks. This is because threats and attacks may not only derive from pitfalls in complex security critical system, but also from ill-designed procedures. However, existing methodologies are not mature enough to embrace procedural implications and the need for multidisciplinary approach on the safe and secure operation of system. This is particularly common in electronic voting (e-voting) systems.

This dissertation focuses along two lines. First, we propose an approach to guarantee a reasonable security to the overall systems by performing formal procedural security analysis. We apply existing techniques and define novel methodologies and approaches for the analysis and verification of procedural rich systems. This includes not only the definition of adequate modeling convention, but also the definition of general techniques for the injection of attacks, and for the transformation of process models into representations that can be given as input to model checkers. With this it is possible to understand and highlight how the switch to the new technological solution changes security, with the ultimate goal of defining the procedures regulating system and system processes that ensure a sufficient level of security for the system as well as for its procedures. We then investigate the usage of formal methods to study and analyze the strength and weaknesses of currently deployed (e-voting) system in order to build the next generation (e-voting) systems. More specifically, we show how formal verification techniques can be used to model and reason about the security of an existing e-voting system. To do that, we reuse the methodology propose for procedural security analysis. The practical applicability of the approaches is demonstrated in several case studies from the domain of public administrations in general and in e-voting system in particular. With this it can be possible to build more secure, reliable, and trustworthy e-voting system.

This thesis presents a method of building executable and interactive application interface prototypes from requirements. The specification of the requirements uses i* and Formal Tropos languages.