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. ^

Directionality based preventive link maintenance scheme for mobile ad hoc networks

The purpose of this study was to design a preventive scheme using directional antennas to improve the performance of mobile ad hoc networks. In this dissertation, a novel Directionality based Preventive Link Maintenance (DPLM) Scheme is proposed to characterize the performance gain [JaY06a, JaY06b, JCY06] by extending the life of link. In order to maintain the link and take preventive action, signal strength of data packets is measured. Moreover, location information or angle of arrival information is collected during communication and saved in the table. When measured signal strength is below orientation threshold , an orientation warning is generated towards the previous hop node. Once orientation warning is received by previous hop (adjacent) node, it verifies the correctness of orientation warning with few hello pings and initiates high quality directional link (a link above the threshold) and immediately switches to it, avoiding a link break altogether. The location information is utilized to create a directional link by orienting neighboring nodes antennas towards each other. We call this operation an orientation handoff, which is similar to soft-handoff in cellular networks. ^ Signal strength is the indicating factor, which represents the health of the link and helps to predict the link failure. In other words, link breakage happens due to node movement and subsequently reducing signal strength of receiving packets. DPLM scheme helps ad hoc networks to avoid or postpone costly operation of route rediscovery in on-demand routing protocols by taking above-mentioned preventive action. ^ This dissertation advocates close but simple collaboration between the routing, medium access control and physical layers. In order to extend the link, the Dynamic Source Routing (DSR) and IEEE 802.11 MAC protocols were modified to use the ability of directional antennas to transmit over longer distance. A directional antenna module is implemented in OPNET simulator with two separate modes of operations: omnidirectional and directional. The antenna module has been incorporated in wireless node model and simulations are performed to characterize the performance improvement of mobile ad hoc networks. Extensive simulations have shown that without affecting the behavior of the routing protocol noticeably, aggregate throughput, packet delivery ratio, end-to-end delay (latency), routing overhead, number of data packets dropped, and number of path breaks are improved considerably. We have done the analysis of the results in different scenarios to evaluate that the use of directional antennas with proposed DPLM scheme has been found promising to improve the performance of mobile ad hoc networks. ^

Enhancement of wireless networks with heterogeneous antennas

In recent years, wireless communication infrastructures have been widely deployed for both personal and business applications. IEEE 802.11 series Wireless Local Area Network (WLAN) standards attract lots of attention due to their low cost and high data rate. Wireless ad hoc networks which use IEEE 802.11 standards are one of hot spots of recent network research. Designing appropriate Media Access Control (MAC) layer protocols is one of the key issues for wireless ad hoc networks. ^ Existing wireless applications typically use omni-directional antennas. When using an omni-directional antenna, the gain of the antenna in all directions is the same. Due to the nature of the Distributed Coordination Function (DCF) mechanism of IEEE 802.11 standards, only one of the one-hop neighbors can send data at one time. Nodes other than the sender and the receiver must be either in idle or listening state, otherwise collisions could occur. The downside of the omni-directionality of antennas is that the spatial reuse ratio is low and the capacity of the network is considerably limited. ^ It is therefore obvious that the directional antenna has been introduced to improve spatial reutilization. As we know, a directional antenna has the following benefits. It can improve transport capacity by decreasing interference of a directional main lobe. It can increase coverage range due to a higher SINR (Signal Interference to Noise Ratio), i.e., with the same power consumption, better connectivity can be achieved. And the usage of power can be reduced, i.e., for the same coverage, a transmitter can reduce its power consumption. ^ To utilizing the advantages of directional antennas, we propose a relay-enabled MAC protocol. Two relay nodes are chosen to forward data when the channel condition of direct link from the sender to the receiver is poor. The two relay nodes can transfer data at the same time and a pipelined data transmission can be achieved by using directional antennas. The throughput can be improved significant when introducing the relay-enabled MAC protocol. ^ Besides the strong points, directional antennas also have some explicit drawbacks, such as the hidden terminal and deafness problems and the requirements of retaining location information for each node. Therefore, an omni-directional antenna should be used in some situations. The combination use of omni-directional and directional antennas leads to the problem of configuring heterogeneous antennas, i e., given a network topology and a traffic pattern, we need to find a tradeoff between using omni-directional and using directional antennas to obtain a better network performance over this configuration. ^ Directly and mathematically establishing the relationship between the network performance and the antenna configurations is extremely difficult, if not intractable. Therefore, in this research, we proposed several clustering-based methods to obtain approximate solutions for heterogeneous antennas configuration problem, which can improve network performance significantly. ^ Our proposed methods consist of two steps. The first step (i.e., clustering links) is to cluster the links into different groups based on the matrix-based system model. After being clustered, the links in the same group have similar neighborhood nodes and will use the same type of antenna. The second step (i.e., labeling links) is to decide the type of antenna for each group. For heterogeneous antennas, some groups of links will use directional antenna and others will adopt omni-directional antenna. Experiments are conducted to compare the proposed methods with existing methods. Experimental results demonstrate that our clustering-based methods can improve the network performance significantly. ^

Two-bit pattern analysis for quantitative information flow

Protecting confidential information from improper disclosure is a fundamental security goal. While encryption and access control are important tools for ensuring confidentiality, they cannot prevent an authorized system from leaking confidential information to its publicly observable outputs, whether inadvertently or maliciously. Hence, secure information flow aims to provide end-to-end control of information flow. Unfortunately, the traditionally-adopted policy of noninterference, which forbids all improper leakage, is often too restrictive. Theories of quantitative information flow address this issue by quantifying the amount of confidential information leaked by a system, with the goal of showing that it is intuitively "small" enough to be tolerated. Given such a theory, it is crucial to develop automated techniques for calculating the leakage in a system. ^ This dissertation is concerned with program analysis for calculating the maximum leakage, or capacity, of confidential information in the context of deterministic systems and under three proposed entropy measures of information leakage: Shannon entropy leakage, min-entropy leakage, and g-leakage. In this context, it turns out that calculating the maximum leakage of a program reduces to counting the number of possible outputs that it can produce. ^ The new approach introduced in this dissertation is to determine two-bit patterns, the relationships among pairs of bits in the output; for instance we might determine that two bits must be unequal. By counting the number of solutions to the two-bit patterns, we obtain an upper bound on the number of possible outputs. Hence, the maximum leakage can be bounded. We first describe a straightforward computation of the two-bit patterns using an automated prover. We then show a more efficient implementation that uses an implication graph to represent the two- bit patterns. It efficiently constructs the graph through the use of an automated prover, random executions, STP counterexamples, and deductive closure. The effectiveness of our techniques, both in terms of efficiency and accuracy, is shown through a number of case studies found in recent literature. ^

Valutazione delle prestazioni di reti ad accesso multiplo basate su visible light communication

Nella società odierna, le telecomunicazioni costituiscono un’esigenza fondamentale della vita quotidiana. Difatti, il mercato della ICT (Information and Communications Technology) è in costante espansione, e viene accompagnato da un rapido sviluppo di nuove tecnologie. In particolare, si assiste a un sempre più rilevante ruolo svolto dalle comunicazioni ottiche, ovvero sfruttanti la luce: in questo contesto, il quale comprende diversi rami ingegneristici, si stanno progressivamente affermando nuove forme di comunicazione basate sulla luce visibile, la cosiddetta Visible Light Communication (VLC). Con questa Tesi ci si propone di implementare con Simulink e stateflow di Matlab il livello MAC (Medium Access Control), basato sullo standard IEEE 802.15.7 per le VLC e valutarne le prestazioni. Prescinde da questa Tesi la parte di implementazione su scheda stessa che è lasciata per sviluppi futuri. Nel capitolo uno si introducono le VLC e si discutono i principali scenari attuali dove possono diffondersi. Nel capitolo 2, si mostrano le principali linee guida afferenti agli standard che sono risultate necessarie per sviluppare lo strato MAC. Nei capitoli 3 e 4 si mostra come il layer sviluppato possa essere utilizzato in due principali situazioni: nel capitolo 3 è descritta la realizzazione di una comunicazione punto-punto, ovvero con un trasmettitore e un ricevitore; nel capitolo 4 è descritta l’implementazione di una rete di nodi, ambito in cui il livello MAC risulta indispensabile. Per ognuna delle situazioni si illustrano scelte e caratteristiche dei sistemi simulati e i risultati ottenuti, cercando di coprire diverse eventualità che intercorrono, più in generale, nella gestione e implementazione di sistemi di telecomunicazione wireless.

SAFE: A Declarative Trust-Agile System with Linked Credentials

Secure Access For Everyone (SAFE), is an integrated system for managing trust

using a logic-based declarative language. Logical trust systems authorize each

request by constructing a proof from a context---a set of authenticated logic

statements representing credentials and policies issued by various principals

in a networked system. A key barrier to practical use of logical trust systems

is the problem of managing proof contexts: identifying, validating, and

assembling the credentials and policies that are relevant to each trust

decision.

SAFE addresses this challenge by (i) proposing a distributed authenticated data

repository for storing the credentials and policies; (ii) introducing a

programmable credential discovery and assembly layer that generates the

appropriate tailored context for a given request. The authenticated data

repository is built upon a scalable key-value store with its contents named by

secure identifiers and certified by the issuing principal. The SAFE language

provides scripting primitives to generate and organize logic sets representing

credentials and policies, materialize the logic sets as certificates, and link

them to reflect delegation patterns in the application. The authorizer fetches

the logic sets on demand, then validates and caches them locally for further

use. Upon each request, the authorizer constructs the tailored proof context

and provides it to the SAFE inference for certified validation.

Delegation-driven credential linking with certified data distribution provides

flexible and dynamic policy control enabling security and trust infrastructure

to be agile, while addressing the perennial problems related to today's

certificate infrastructure: automated credential discovery, scalable

revocation, and issuing credentials without relying on centralized authority.

We envision SAFE as a new foundation for building secure network systems. We

used SAFE to build secure services based on case studies drawn from practice:

(i) a secure name service resolver similar to DNS that resolves a name across

multi-domain federated systems; (ii) a secure proxy shim to delegate access

control decisions in a key-value store; (iii) an authorization module for a

networked infrastructure-as-a-service system with a federated trust structure

(NSF GENI initiative); and (iv) a secure cooperative data analytics service

that adheres to individual secrecy constraints while disclosing the data. We

present empirical evaluation based on these case studies and demonstrate that

SAFE supports a wide range of applications with low overhead.

Multidimensional Intrusion Detection System for IEC 61850 based SCADA Networks

Emerging cybersecurity vulnerabilities in supervisory control and data acquisition (SCADA) systems are becoming urgent engineering issues for modern substations. This paper proposes a novel intrusion detection system (IDS) tailored for cybersecurity of IEC 61850 based substations. The proposed IDS integrates physical knowledge, protocol specifications and logical behaviours to provide a comprehensive and effective solution that is able to mitigate various cyberattacks. The proposed approach comprises access control detection, protocol whitelisting, model-based detection, and multi-parameter based detection. This SCADA-specific IDS is implemented and validated using a comprehensive and realistic cyber-physical test-bed and data from a real 500kV smart substation.

Rede de controle em ambiente hospitalar: um protocolo multiciclos para automação hospitalar sobre IEEE 802.3 com IGMP Snooping

VALENTIM, R. A. M. ; MORAIS, A. H. F. ; SOUZA, V. S. V ; ARAUJO JUNIOR, H. B. ; BRANDAO, G. B. ; GUERREIRO, A. M. G. . Rede de Controle em Ambiente Hospitalar: um protocolo multiciclos para automação hospitalar sobre IEEE 802.3 com IGMP Snooping. Revista Ciência e Tecnologia, v. 11, p. 19, 2009

Rede de controle em ambiente hospitalar: um protocolo multiciclos para automação hospitalar sobre IEEE 802.3 com IGMP Snooping

VALENTIM, R. A. M. ; MORAIS, A. H. F. ; SOUZA, V. S. V ; ARAUJO JUNIOR, H. B. ; BRANDAO, G. B. ; GUERREIRO, A. M. G. . Rede de Controle em Ambiente Hospitalar: um protocolo multiciclos para automação hospitalar sobre IEEE 802.3 com IGMP Snooping. Revista Ciência e Tecnologia, v. 11, p. 19, 2009

An E-government Interoperability Platform Supporting Personal Data Protection Regulations

Public agencies are increasingly required to collaborate with each other in order to provide high-quality e-government services. This collaboration is usually based on the service-oriented approach and supported by interoperability platforms. Such platforms are specialized middleware-based infrastructures enabling the provision, discovery and invocation of interoperable software services. In turn, given that personal data handled by governments are often very sensitive, most governments have developed some sort of legislation focusing on data protection. This paper proposes solutions for monitoring and enforcing data protection laws within an E-government Interoperability Platform. In particular, the proposal addresses requirements posed by the Uruguayan Data Protection Law and the Uruguayan E-government Platform, although it can also be applied in similar scenarios. The solutions are based on well-known integration mechanisms (e.g. Enterprise Service Bus) as well as recognized security standards (e.g. eXtensible Access Control Markup Language) and were completely prototyped leveraging the SwitchYard ESB product.

Protecting databases from schema disclosure: a CRUD-based protection model

Database schemas, in many organizations, are considered one of the critical assets to be protected. From database schemas, it is not only possible to infer the information being collected but also the way organizations manage their businesses and/or activities. One of the ways to disclose database schemas is through the Create, Read, Update and Delete (CRUD) expressions. In fact, their use can follow strict security rules or be unregulated by malicious users. In the first case, users are required to master database schemas. This can be critical when applications that access the database directly, which we call database interface applications (DIA), are developed by third party organizations via outsourcing. In the second case, users can disclose partially or totally database schemas following malicious algorithms based on CRUD expressions. To overcome this vulnerability, we propose a new technique where CRUD expressions cannot be directly manipulated by DIAs any more. Whenever a DIA starts-up, the associated database server generates a random codified token for each CRUD expression and sends it to the DIA that the database servers can use to execute the correspondent CRUD expression. In order to validate our proposal, we present a conceptual architectural model and a proof of concept.

ABTC: multi-purpose adaptable business tier components based on Call Level Interfaces

Call Level Interfaces (CLI) are low level API that play a key role in database applications whenever a fine tune control between application tiers and the host databases is a key requirement. Unfortunately, in spite of this significant advantage, CLI were not designed to address organizational requirements and contextual runtime requirements. Among the examples we emphasize the need to decouple or not to decouple the development process of business tiers from the development process of application tiers and also the need to automatically adapt to new business and/or security needs at runtime. To tackle these CLI drawbacks, and simultaneously keep their advantages, this paper proposes an architecture relying on CLI from which multi-purpose business tiers components are built, herein referred to as Adaptable Business Tier Components (ABTC). This paper presents the reference architecture for those components and a proof of concept based on Java and Java Database Connectivity (an example of CLI).

An efficient MAC protocol with adaptive energy harvesting for machine-to-machine networks

In a machine-to-machine network, the throughput performance plays a very important role. Recently, an attractive energy harvesting technology has shown great potential to the improvement of the network throughput, as it can provide consistent energy for wireless devices to transmit data. Motivated by that, an efficient energy harvesting-based medium access control (MAC) protocol is designed in this paper. In this protocol, different devices first harvest energy adaptively and then contend the transmission opportunities with energy level related priorities. Then, a new model is proposed to obtain the optimal throughput of the network, together with the corresponding hybrid differential evolution algorithm, where the involved variables are energy-harvesting time, contending time, and contending probability. Analytical and simulation results show that the network based on the proposed MAC protocol has greater throughput than that of the traditional methods. In addition, as expected, our scheme has less transmission delay, further enhancing its superiority.

SEMD: secure and efficient message dissemination with policy enforcement in VANET

Vehicular ad hoc network (VANET) is an increasing important paradigm, which not only provides safety enhancement but also improves roadway system efficiency. However, the security issues of data confidentiality, and access control over transmitted messages in VANET have remained to be solved. In this paper, we propose a secure and efficient message dissemination scheme (SEMD) with policy enforcement in VANET, and construct an outsourcing decryption of ciphertext-policy attribute-based encryption (CP-ABE) to provide differentiated access control services, which makes the vehicles delegate most of the decryption computation to nearest roadside unit (RSU). Performance evaluation demonstrates its efficiency in terms of computational complexity, space complexity, and decryption time. Security proof shows that it is secure against replayable choosen-ciphertext attacks (RCCA) in the standard model.

Efectos de una intervención educativa en los conocimientos y comportamientos relacionados con la fotoprotección durante la práctica de la actividad física en los estudiantes de un colegio público de Bogotá D.C., Colombia

Introducción: La incidencia del cáncer de piel melanoma y no melanoma es un problema de salud pública a nivel mundial. El incremento en la incidencia del cáncer de piel en los últimos años se debe a múltiples factores como: cambios en los estilos de vida, el envejecimiento de la población, cambios ambientales, el desconocimiento a la exposición a la radiación ultravioleta (RUV) durante la práctica de actividad física sin elementos de fotoprotección, siendo éste último reconocido como el principal factor de riesgo. Objetivo: Evaluar los efectos de una intervención educativa en los conocimientos y comportamientos relacionados con la fotoprotección durante la práctica de la actividad física en estudiantes de un colegio público de Bogotá D.C., Colombia. Métodos: Estudio de intervención, antes y después, no controlado en 281 estudiantes de los grados noveno, décimo y once de estratos 1-3 de un colegio público de Bogotá, con seguimiento a 1, 3 y 6 meses post-intervención. Se evaluaron los conocimientos y los hábitos de fotoprotección mediante un cuestionario Cancer Awareness Measure (CAM) y el modelo Transteórico de cambio comportamental de Prochaska y Di Clemente. El estudio se realizó durante el primer semestre de 2015 con 4 sesiones educativas de 60 minutos apoyadas con material audiovisual y pedagógico, acorde a la Guía para la Comunicación Educativa en el marco el control del cáncer publicada por el Instituto Nacional de Cancerología. Resultados: Del grupo de estudiantes que participaron del estudio, el 52,3% eran hombres, el promedio de edad fue de 15,46 ± 1,2 años. El tipo de piel predominante fue la trigueña con 65,8%. La intervención educativa produjo cambios significativos en los conocimientos de foto protección, finalizado el seguimiento al sexto mes. En cuanto a la prevención los estudiantes refirieron tener conocimiento de cómo examinar su piel en el momento basal (12,5% n=35), presentándose un aumento significativo de 62,6% (n=211) al sexto mes (p<0,05). Conclusión: El estudio demostró la efectividad de la intervención educativa, evidenciando cambios significativos en los conocimientos en fotoprotección y comportamientos preventivos del cáncer de piel durante la práctica de la actividad física en estudiantes de un colegio público de Bogotá D.C., Colombia.