Evaluation of binary decision diagrams for redundancy, shadowing, generalisation and correlation in an Information sharing model.

This paper defines a structured methodology which is based on the foundational work of Al-Shaer et al. in [1] and that of Hamed and Al-Shaer in [2]. It defines a methodology for the declaration of policy field elements, through to the syntax, ontology and functional verification stages. In their works of [1] and [2] the authors concentrated on developing formal definitions of possible anomalies between rules in a network firewall rule set. Their work is considered as the foundation for further works on anomaly detection, including those of Fitzgerald et al. [3], Chen et al. [4], Hu et al. [5], among others. This paper extends this work by applying the methods to information sharing policies, and outlines the evaluation related to these.

Evaluation of TFTP DDoS Amplification Attack.

Web threats are becoming a major issue for both governments and companies. Generally, web threats increased as much as 600% during last year (WebSense, 2013). This appears to be a significant issue, since many major businesses seem to provide these services. Denial of Service (DoS) attacks are one of the most significant web threats and generally their aim is to waste the resources of the target machine (Mirkovic & Reiher, 2004). Dis-tributed Denial of Service (DDoS) attacks are typically executed from many sources and can result in large traf-fic flows. During last year 11% of DDoS attacks were over 60 Gbps (Prolexic, 2013a). The DDoS attacks are usually performed from the large botnets, which are networks of remotely controlled computers. There is an increasing effort by governments and companies to shut down the botnets (Dittrich, 2012), which has lead the attackers to look for alternative DDoS attack methods. One of the techniques to which attackers are returning to is DDoS amplification attacks. Amplification attacks use intermediate devices called amplifiers in order to amplify the attacker's traffic. This work outlines an evaluation tool and evaluates an amplification attack based on the Trivial File Transfer Proto-col (TFTP). This attack could have amplification factor of approximately 60, which rates highly alongside other researched amplification attacks. This could be a substantial issue globally, due to the fact this protocol is used in approximately 599,600 publicly open TFTP servers. Mitigation methods to this threat have also been consid-ered and a variety of countermeasures are proposed. Effects of this attack on both amplifier and target were analysed based on the proposed metrics. While it has been reported that the breaching of TFTP would be possible (Schultz, 2013), this paper provides a complete methodology for the setup of the attack, and its verification.

Detecting False Identity through Behavioural Patterns

T. Boongoen and Q. Shen. 'Detecting False Identity through Behavioural Patterns', In Proceedings of International Crime Science Conference, British Library, London UK, 2008. Publisher's online version forthcoming.;The full text is currently unavailable in CADAIR pending approval by the publisher. Sponsorship: UK EPSRC grant EP/D057086

Ewaluacja splotowa InfoKultury. Skala dwuważonych ocen

Pakiet oprogramowania InfoCult™ Analyser 1.4 stanowiącego obudowę książki do pobrania ze strony: ewaluacja.amu.edu.pl

Zintegrowane kształcenie przedmiotowo-językowe. Dydaktyka zadaniowa a rozwój osobistej kompetencji komunikacyjnej w warunkach półautonomii

Wydział Neofilologii

Herod Wielki i „nowa” Jerozolima

Summary: Herod the Great (73-4 B.C.E.) was a Roman client king of the small Jewish state Judaea in the last three decades before the common era. An essential aspect of Herod's reign was his role as a builder. Remarkably innovative, he created an astonishing record of architectural achievement, not only in Judaea but also throughout Greece and the Roman East. Herod’s own inclinations caused him to engage in a building program that paralleled that of his patron, Augustus. The most famous and ambitious project was the expansion of Jerusalem and rebuilding of the Second Temple. Josephus Flavius, a 1st-century Jewish historian, in his descriptions of the visual structure of Jerusalem delivers the picture of the Jewish society in the latter Second Temple Judaea, who were fundamentally antagonistic toward images. For Josephus, Roman iconography, such as Herod’s eagle from the Jerusalem Temple, represents not only political domination but also an unambiguous religious abomination. Visual conservatism in the public realm finds important verification in the excavated remains of Jerusalem’s Temple Mount and the Herodian Quarter (Upper City). Geometric patterns and forms predominate on the floor mosaic, stone furniture, in architectural detail and funerary remains. No human imagery is present in the Jewish context. However, Herodian structures in Jerusalem reflect the architectural and visual vocabulary of their time which contains popular elements of Roman domination in the ancient world.

Zagadnienia wykładni prawa w unijnych kontekstach interpretacyjnych. O adekwatności i możliwych rozwinięciach derywacyjnej koncepcji wykładni

Wydział Prawa i Administracji

Zinstytucjonalizowane sieci współdziałania międzygminnego w Polsce

Podstawowym problemem badawczym rozprawy doktorskiej mgra Bartłomieja Kołsuta jest powstawanie i funkcjonowanie zinstytucjonalizowanych sieci współdziałania międzygminnego w Polsce. W pracy skoncentrowano się na realizacji pięciu najważniejszych celów poznawczych. Dotyczą one: 1. identyfikacji zinstytucjonalizowanych sieci współdziałania międzygminnego w Polsce według stanu na koniec 2014 roku, 2. typologii funkcjonalnej zidentyfikowanych sieci, 3. próby wyjaśnienia przyczyn powstawania sieci w okresie 1990-2014, 4. weryfikacji wybranych czynników usieciowienia gmin, 5. próby oceny przydatności wybranych teorii instytucjonalnych w wyjaśnianiu przyczyn powstawania i funkcjonowania sieci. W rozprawie wykorzystano szereg metod i technik badawczych, m. in. metodę analizy treści, statystyczne miary współzmienności (współczynnik phi Yule’a, iloraz szans, współczynnik korelacji liniowej Pearsona). W procesie identyfikacji sieci przeanalizowano ponad 2,5 tys. dokumentów i opracowań, korzystając przy tym z kilkudziesięciu, różnego rodzaju baz danych. Wyniki przeprowadzonych badań empirycznych pozwoliły także dokonać oceny przydatności teorii instytucjonalnych (m. in. instytucjonalizmu wyboru racjonalnego, instytucjonalizmu socjologicznego oraz instytucjonalizmu historycznego) w wyjaśnianiu przyczyn powstawania i funkcjonowania sieci. Zrealizowana rozprawa jest pierwszym tak kompleksowym i pogłębionym opracowaniem geograficznego wymiaru zinstytucjonalizowanej współpracy międzygminnej w Polsce.

Era uma vez dentro de nós!

Dissertação apresentada à Universidade Fernando Pessoa como parte dos requisitos para obtenção do grau de Mestre em Criatividade e Inovação

SOUND PROPAGATION AND SCATTERING IN BUBBLY LIQUIDS

In the ocean, natural and artificial processes generate clouds of bubbles which scatter and attenuate sound. Measurements have shown that at the individual bubble resonance frequency, sound propagation in this medium is highly attenuated and dispersive. Theory to explain this behavior exists in the literature, and is adequate away from resonance. However, due to excessive attenuation near resonance, little experimental data exists for comparison. An impedance tube was developed specifically for exploring this regime. Using the instrument, unique phase speed and attenuation measurements were made for void fractions ranging from 6.2 × 10^−5 to 2.7 × 10^−3 and bubble sizes centered around 0.62 mm in radius. Improved measurement speed, accuracy and precision is possible with the new instrument, and both instantaneous and time-averaged measurements were obtained. Behavior at resonance was observed to be sensitive to the bubble population statistics and agreed with existing theory, within the uncertainty of the bubble population parameters. Scattering from acoustically compact bubble clouds can be predicted from classical scattering theory by using an effective medium description of the bubbly fluid interior. Experimental verification was previously obtained up to the lowest resonance frequency. A novel bubble production technique has been employed to obtain unique scattering measurements with a bubbly-liquid-filled latex tube in a large indoor tank. The effective scattering model described these measurements up to three times the lowest resonance frequency of the structure.

HEATING IN VASCULAR TISSUE AND FLOW-THROUGH TISSUE PHANTOMS INDUCED BY FOCUSED ULTRASOUND

High intensity focused ultrasound (HIFU) can be used to control bleeding, both from individual blood vessels as well as from gross damage to the capillary bed. This process, called acoustic hemostasis, is being studied in the hope that such a method would ultimately provide a lifesaving treatment during the so-called "golden hour", a brief grace period after a severe trauma in which prompt therapy can save the life of an injured person. Thermal effects play a major role in occlusion of small vessels and also appear to contribute to the sealing of punctures in major blood vessels. However, aggressive ultrasound-induced tissue heating can also impact healthy tissue and can lead to deleterious mechanical bioeffects. Moreover, the presence of vascularity can limit one’s ability to elevate the temperature of blood vessel walls owing to convective heat transport. In an effort to better understand the heating process in tissues with vascular structure we have developed a numerical simulation that couples models for ultrasound propagation, acoustic streaming, ultrasound heating and blood cooling in Newtonian viscous media. The 3-D simulation allows for the study of complicated biological structures and insonation geometries. We have also undertaken a series of in vitro experiments, in non-uniform flow-through tissue phantoms, designed to provide a ground truth verification of the model predictions. The calculated and measured results were compared over a range of values for insonation pressure, insonation time, and flow rate; we show good agreement between predictions and measurements. We then conducted a series of simulations that address two limiting problems of interest: hemostasis in small and large vessels. We employed realistic human tissue properties and considered more complex geometries. Results show that the heating pattern in and around a blood vessel is different for different vessel sizes, flow rates and for varying beam orientations relative to the flow axis. Complete occlusion and wall- puncture sealing are both possible depending on the exposure conditions. These results concur with prior clinical observations and may prove useful for planning of a more effective procedure in HIFU treatments.

Safe Compositional Network Sketches: NetSketch Tool Implementation

Numerous problems exist that can be modeled as traffic through a network in which constraints exist to regulate flow. Vehicular road travel, computer networks, and cloud based resource distribution, among others all have natural representations in this manner. As these networks grow in size and/or complexity, analysis and certification of the safety invariants becomes increasingly costly. The NetSketch formalism introduces a lightweight verification framework that allows for greater scalability than traditional analysis methods. The NetSketch tool was developed to provide the power of this formalism in an easy to use and intuitive user interface.

Building Responsive Systems from Physically-correct Specifications

Predictability - the ability to foretell that an implementation will not violate a set of specified reliability and timeliness requirements - is a crucial, highly desirable property of responsive embedded systems. This paper overviews a development methodology for responsive systems, which enhances predictability by eliminating potential hazards resulting from physically-unsound specifications. The backbone of our methodology is the Time-constrained Reactive Automaton (TRA) formalism, which adopts a fundamental notion of space and time that restricts expressiveness in a way that allows the specification of only reactive, spontaneous, and causal computation. Using the TRA model, unrealistic systems - possessing properties such as clairvoyance, caprice, in finite capacity, or perfect timing - cannot even be specified. We argue that this "ounce of prevention" at the specification level is likely to spare a lot of time and energy in the development cycle of responsive systems - not to mention the elimination of potential hazards that would have gone, otherwise, unnoticed. The TRA model is presented to system developers through the CLEOPATRA programming language. CLEOPATRA features a C-like imperative syntax for the description of computation, which makes it easier to incorporate in applications already using C. It is event-driven, and thus appropriate for embedded process control applications. It is object-oriented and compositional, thus advocating modularity and reusability. CLEOPATRA is semantically sound; its objects can be transformed, mechanically and unambiguously, into formal TRA automata for verification purposes, which can be pursued using model-checking or theorem proving techniques. Since 1989, an ancestor of CLEOPATRA has been in use as a specification and simulation language for embedded time-critical robotic processes.

OS Support for Portable Bulk Synchronous Parallel Programs

Predictability -- the ability to foretell that an implementation will not violate a set of specified reliability and timeliness requirements -- is a crucial, highly desirable property of responsive embedded systems. This paper overviews a development methodology for responsive systems, which enhances predictability by eliminating potential hazards resulting from physically-unsound specifications. The backbone of our methodology is the Time-constrained Reactive Automaton (TRA) formalism, which adopts a fundamental notion of space and time that restricts expressiveness in a way that allows the specification of only reactive, spontaneous, and causal computation. Using the TRA model, unrealistic systems – possessing properties such as clairvoyance, caprice, infinite capacity, or perfect timing -- cannot even be specified. We argue that this "ounce of prevention" at the specification level is likely to spare a lot of time and energy in the development cycle of responsive systems -- not to mention the elimination of potential hazards that would have gone, otherwise, unnoticed. The TRA model is presented to system developers through the Cleopatra programming language. Cleopatra features a C-like imperative syntax for the description of computation, which makes it easier to incorporate in applications already using C. It is event-driven, and thus appropriate for embedded process control applications. It is object-oriented and compositional, thus advocating modularity and reusability. Cleopatra is semantically sound; its objects can be transformed, mechanically and unambiguously, into formal TRA automata for verification purposes, which can be pursued using model-checking or theorem proving techniques. Since 1989, an ancestor of Cleopatra has been in use as a specification and simulation language for embedded time-critical robotic processes.

Safe Composition of Web Communication Protocols for Extensible Edge Services

As new multi-party edge services are deployed on the Internet, application-layer protocols with complex communication models and event dependencies are increasingly being specified and adopted. To ensure that such protocols (and compositions thereof with existing protocols) do not result in undesirable behaviors (e.g., livelocks) there needs to be a methodology for the automated checking of the "safety" of these protocols. In this paper, we present ingredients of such a methodology. Specifically, we show how SPIN, a tool from the formal systems verification community, can be used to quickly identify problematic behaviors of application-layer protocols with non-trivial communication models—such as HTTP with the addition of the "100 Continue" mechanism. As a case study, we examine several versions of the specification for the Continue mechanism; our experiments mechanically uncovered multi-version interoperability problems, including some which motivated revisions of HTTP/1.1 and some which persist even with the current version of the protocol. One such problem resembles a classic degradation-of-service attack, but can arise between well-meaning peers. We also discuss how the methods we employ can be used to make explicit the requirements for hardening a protocol's implementation against potentially malicious peers, and for verifying an implementation's interoperability with the full range of allowable peer behaviors.