User Behavioral Modeling of Web-based Systems for Continuous User Authentication

Authentication plays an important role in how we interact with computers, mobile devices, the web, etc. The idea of authentication is to uniquely identify a user before granting access to system privileges. For example, in recent years more corporate information and applications have been accessible via the Internet and Intranet. Many employees are working from remote locations and need access to secure corporate files. During this time, it is possible for malicious or unauthorized users to gain access to the system. For this reason, it is logical to have some mechanism in place to detect whether the logged-in user is the same user in control of the user's session. Therefore, highly secure authentication methods must be used. We posit that each of us is unique in our use of computer systems. It is this uniqueness that is leveraged to "continuously authenticate users" while they use web software. To monitor user behavior, n-gram models are used to capture user interactions with web-based software. This statistical language model essentially captures sequences and sub-sequences of user actions, their orderings, and temporal relationships that make them unique by providing a model of how each user typically behaves. Users are then continuously monitored during software operations. Large deviations from "normal behavior" can possibly indicate malicious or unintended behavior. This approach is implemented in a system called Intruder Detector (ID) that models user actions as embodied in web logs generated in response to a user's actions. User identification through web logs is cost-effective and non-intrusive. We perform experiments on a large fielded system with web logs of approximately 4000 users. For these experiments, we use two classification techniques; binary and multi-class classification. We evaluate model-specific differences of user behavior based on coarse-grain (i.e., role) and fine-grain (i.e., individual) analysis. A specific set of metrics are used to provide valuable insight into how each model performs. Intruder Detector achieves accurate results when identifying legitimate users and user types. This tool is also able to detect outliers in role-based user behavior with optimal performance. In addition to web applications, this continuous monitoring technique can be used with other user-based systems such as mobile devices and the analysis of network traffic.

Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

Formal Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Pré-regulador retificador boost com controle digital por valores médios, para sistema de iluminação fluorescente multi-lâmpadas, utilizando dispositivo FPGA e VHDL

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Papel da serotonina no comportamento defensivo do paulistinha (Danio rerio Hamilton 1822) adulto: Diferenças entre modelos comportamentais, linhagens, e efeitos do estresse predatório agudo

Os transtornos de ansiedade apresentam a maior incidência na população mundial dentre os transtornos psiquiátricos, e a eficácia clínica das drogas ansiolíticas é baixa, em parte devido ao desconhecimento acerca das bases neuroquímicas desses transtornos. Para uma compreensão mais ampla e evolutivamente substanciada desses fenômenos, a utilização de espécies filogeneticamente mais antigas pode ser uma aproximação interessante no campo da modelagem comportamental; assim, sugerimos o uso do paulistinha (Danio rerio Hamilton 1822) na tentativa de compreender a modulação de comportamentos tipo-ansiedade pelo sistema serotonérgico. Demonstramos que os níveis extracelulares de serotonina no encéfalo de paulistinhas adultos expostos ao teste de preferência claro/escuro [PCE] (mas não ao teste de distribuição vertical eliciada pela novidade [DVN]) apresentam-se elevados em relação a animais manipulados mas não expostos aos aparatos. Além disso, os níveis teciduais de serotonina no rombencéfalo e no prosencéfalo são elevados pela exposição ao PCE, enquanto no mesencéfalo são elevados pela exposição ao DVN. Os níveis extracelulares de serotonina estão correlacionados negativamente com a geotaxia no DVN, e positivamente com a escototaxia, tigmotaxia e a avaliação de risco no PCE. O tratamento agudo com uma dose baixa de fluoxetina (2,5 mg/kg) aumenta a escototaxia, a tigmotaxia e a avaliação de risco no PCE, diminui a geotaxia e o congelamento e facilita a habituação no DVN. O tratamento com buspirona diminui a escototaxia, a tigmotaxia e o congelamento nas doses de 25 e 50 mg/kg no PCE, e diminui a avaliação de risco na dose de 50 mg/kg; no DVN, ambas as doses diminuem a geotaxia, enquanto somente a maior dose diminui o congelamento e facilita a habituação. O tratamento com WAY 100635 diminui a escototaxia nas doses de 0,003 e 0,03 mg/kg, enquanto somente a dose de 0,03 mg/kg diminui a tigmotaxia e a avaliação de risco no PCE. No DVN, ambas as doses diminuem a geotaxia, enquanto somente a menor dose facilita a habituação e aumenta o tempo em uma “base” (“homebase”). O tratamento com SB 224289 não produziu efeitos sobre a escototaxia, mas aumentou a avaliação de risco na dose de 2,5 mg/kg; no DVN, essa droga diminuiu a geotaxia e o nado errático nas doses de 2,5 e 5 mg/kg, enquanto a dose de 2,5 mg/kg aumentou a formação de “bases”. O tratamento com DL-para-clorofenilalanina (2 injeções de 300 mg/kg, separadas por 24 horas) diminuiu a escototaxia, a tigmotaxia e a avaliação de risco no PCE, aumentou a geotaxia e a formação de bases e diminuiu a habituação no DVN. Quando os animais são pré-expostos a uma “substância de alarme” co-específica, observa-se um aumento nos níveis extracelulares de serotonina associados a um aumento na escototaxia, congelamento e nado errático no PCE; os efeitos comportamentais e neuroquímicos foram bloqueados pelo pré tratamento com fluoxetina (2,5 mg/kg), mas não pelo pré-tratamento com WAY 100,635 (0,003 mg/kg). Animais da linhagem leopard apresentam maior escototaxia e avaliação de risco no PCE, assim como níveis teciduais elevados de serotonina no encéfalo; o fenótipo comportamental é resgatado pelo tratamento com fluoxetina (5 mg/kg). Esses dados sugerem que o sistema serotonérgico dessa espécie modula o comportamento no DVN e no PCE de forma oposta; que a resposta de medo produzida pela substância de alarme também parece aumentar a atividade do sistema serotonérgico, um efeito possivelmente mediado pelos transportadores de serotonina, e ao menos um fenótipo mutante de alta ansiedade também está associado a esses transportadores. Sugere-se que, de um ponto de vista funcional, a serotonina aumenta a ansiedade e diminui o medo em paulistinhas.

The Assessment of Multiple Processes Underlying the Attentional Blink: A Fixed - links Modeling Approach based on Behavioral and Electrophysiological Data

When observers are presented with two visual targets appearing in the same position in close temporal proximity, a marked reduction in detection performance of the second target has often been reported, the so-called attentional blink phenomenon. Several studies found a similar decrement of P300 amplitudes during the attentional blink period as observed with detection performances of the second target. However, whether the parallel courses of second target performances and corresponding P300 amplitudes resulted from the same underlying mechanisms remained unclear. The aim of our study was therefore to investigate whether the mechanisms underlying the AB can be assessed by fixed-links modeling and whether this kind of assessment would reveal the same or at least related processes in the behavioral and electrophysiological data. On both levels of observation three highly similar processes could be identified: an increasing, a decreasing and a u-shaped trend. Corresponding processes from the behavioral and electrophysiological data were substantially correlated, with the two u-shaped trends showing the strongest association with each other. Our results provide evidence for the assumption that the same mechanisms underlie attentional blink task performance at the electrophysiological and behavioral levels as assessed by fixed-links models.

A fixed-links modeling approach to assess individual differences in the attentional blink: Analysis of behavioral and psychophysiological data

The attentional blink (AB) is a fundamental limitation of the ability to select relevant information from irrelevant information. It can be observed with the detection rate in an AB task as well as with the corresponding P300 amplitude of the event-related potential. In previous research, however, correlations between these two levels of observation were weak and rather inconsistent. A possible explanation of this finding might be that multiple processes underlie the AB and, thus, obscure a possible relationship between AB-related detection rate and the corresponding P300 amplitude. The present study investigated this assumption by applying a fixed-links modeling approach to represent behavioral individual differences in the AB as a latent variable. Concurrently, this approach enabled us to control for additional sources of variance in AB performance by deriving two additional latent variables. The correlation between the latent variable reflecting behavioral individual differences in AB magnitude and a corresponding latent variable derived from the P300 amplitude was high (r=.70). Furthermore, this correlation was considerably stronger than the correlations of other behavioral measures of the AB magnitude with their psychophysiological counterparts (all rs<.40). Our findings clearly indicate that the systematic disentangling of various sources of variance by utilizing the fixed-links modeling approach is a promising tool to investigate behavioral individual differences in the AB and possible psychophysiological correlates of these individual differences.

The neural development and organization of letter recognition: Evidence from functional neuroimaging, computational modeling, and behavioral studies

Although much of the brain’s functional organization is genetically predetermined, it appears that some noninnate functions can come to depend on dedicated and segregated neural tissue. In this paper, we describe a series of experiments that have investigated the neural development and organization of one such noninnate function: letter recognition. Functional neuroimaging demonstrates that letter and digit recognition depend on different neural substrates in some literate adults. How could the processing of two stimulus categories that are distinguished solely by cultural conventions become segregated in the brain? One possibility is that correlation-based learning in the brain leads to a spatial organization in cortex that reflects the temporal and spatial clustering of letters with letters in the environment. Simulations confirm that environmental co-occurrence does indeed lead to spatial localization in a neural network that uses correlation-based learning. Furthermore, behavioral studies confirm one critical prediction of this co-occurrence hypothesis, namely, that subjects exposed to a visual environment in which letters and digits occur together rather than separately (postal workers who process letters and digits together in Canadian postal codes) do indeed show less behavioral evidence for segregated letter and digit processing.

Behavioral Types for Embedded Software - A Survey

At present, there is a variety of formalisms for modeling and analyzing the communication behavior of components. Due to a tremendous increase in size and complexity of embedded systems accompanied by shorter time to market cycles and cost reduction, so called behavioral type systems become more and more important. This chapter presents an overview and a taxonomy of behavioral types. The intentions of this taxonomy are to provide a guidance for software engineers and to form the basis for future research.

Direction of Causation Modeling Between Cross-Sectional Measures of Parenting and Psychological Distress in Female Twins

Under certain conditions, cross-sectional analysis of cross-twin intertrait correlations can provide important information about the direction of causation (DOC) between two variables. A community-based sample of Australian female twins aged 18 to 45 years was mailed an extensive Health and Lifestyle Questionnaire (HLQ) that covered a wide range of personality and behavioral measures. Included were self-report measures of recent psychological distress and perceived childhood environment (PBI). Factor analysis of the PBI yielded three interpretable dimensions: Coldness, Overprotection, and Autonomy. Univariate analysis revealed that parental Overprotection and Autonomy were best explained by additive genetic, shared, and nonshared environmental effects (ACE), whereas the best-fitting model for PBI Coldness and the three measures of psychological distress (Depression, Phobic Anxiety, and Somatic Distress) included only additive genetic and nonshared environmental effects (AE). A common pathway model best explained the covariation between (1) the three PBI dimensions and (2) the three measures of psychological distress. DOC modeling between latent constructs of parenting and psychological distress revealed that a model which specified recollected parental behavior as the cause of psychological distress provided a better fit than a model which specified psychological distress as the cause of recollected parental behavior. Power analyses and limitations of the findings are discussed.

Assessing organizations collaboration readiness: a behavioral approach

Dissertation presented at the Faculty of Sciences and Technology of the New University of Lisbon to obtain the degree of Doctor in Electrical Engineering, specialty of Robotics and Integrated Manufacturing