In NGAC (Next Generation Access Control) systems, an access event can trigger concurrent obligations that dynamically modify authorization policy elements and, consequently, user privileges. A race condition arises when the resulting privileges depend on the execution order of these obligations, potentially causing serious security issues such as privilege escalation or denial of service. Although race conditions have been extensively studied in other computing systems, they pose a novel challenge in access control because NGAC introduces concurrent, privilege-changing obligations. To address this challenge, this paper investigates the use of SMT (Satisfiability Modulo Theories) to detect their presence. The SMT encoding approach precisely captures the procedural semantics of obligations, allowing for a thorough analysis of interdependence within obligations and between concurrent obligations. We implemented this approach using the NGAC reference implementation and the CVC5 SMT solver, and applied it to real-world systems. The results demonstrate that our approach can effectively identify obligation races.

Modern legal proceedings rely on diverse digital evidence, highlighting the need for efficient forensic identification in unstructured legal documents. This paper introduces a framework that leverages Large Language Models (LLMs) to identify forensic evidence entities, extract their relationships from legal documents, and reconstruct Judicial Digital Forensic Evidence Graphs (JDFEGs) using the entities and relationships. In our approach, we first formalize JDFEGs by defining judicial entities and relationships in the legal domain. Then, we present a structured, goal-oriented prompt design for reconstructing JDFEGs step by step. We apply our approach to five real-world legal documents to evaluate the accuracy of the reconstructed JDFEGs, incorporating k-shot learning. The empirical study results show that incorporating few-shot prompting significantly improves the accuracy and completeness of reconstructed JDFEG with an 86% F1-score and relationships with a 68% F1-score, cutting the error rate by more than half compared to zero-shot baselines. These findings highlight the potential of LLMs to enhance digital forensic analysis and judicial decision-making.

Transitioning legacy C codebases to Rust has emerged as a promising approach to addressing memory safety issues inherent in C. However, existing methods often produce non-idiomatic or semantically inconsistent Rust code. This paper introduces C2RustTV, a framework that leverages large language models (LLMs) to translate C programs to idiomatic Rust code while assuring translation quality through automated conformance testing. C2RustTV integrates test case generation, automated translation of both production and test code, and conformance validation via test execution. Experiments across multiple datasets demonstrate the effectiveness of C2RustTV, achieving higher rates of compilation success and functional conformance compared to state-of-the-art techniques.

Software development is undergoing a revolutionary transformation, fueled by remarkable advancements in Large Language Models (LLMs). This wave of innovation is reshaping the entire landscape and holds the promise of streamlining the development process, leading to increased productivity and efficiency. By providing text prompts, developers can now receive entirely generated code outputs, representing a fundamental shift in how software is built. This paradigm change can accelerate development cycles and unlock new levels of creativity and ingenuity, resulting in the realization of novel applications and business outcomes. However, this paradigm shift also brings new challenges and necessitates acquiring additional skills for software developers to fully harness the capabilities of LLM-powered tools. These skills include prompt engineering for software development, structural complexity management, debugging of AI errors, and compliance with ethical guidelines and principles.

As large language models (LLMs) evolve into autonomous agents equipped with tools and communication capabilities, they are increasingly deployed in multi-agent systems (MASs) to perform complex tasks. While these systems offer new levels of functionality and efficiency, their security risks remain underexplored. In this paper, we present a focused security analysis of LLM agents by implementing six representative attacks on two real-world MASs. These attacks expose structural and behavioral vulnerabilities unique to agent-based systems. We also introduce and evaluate defensive mechanisms such as fine-tuned agent behaviors, access control via the NGAC (Next Generation Access Control) standard, and a novel "sanity checker" agent for validating agent outputs. Our findings highlight the urgent need for robust, standardized security frameworks for LLM-based MASs and suggest promising directions for future research in agent-level threat modeling and mitigation.

The Structured Threat Information Expression (STIX) standard has become essential for representing and sharing cyber threat intelligence (CTI). However, automatically generating valid and semantically consistent STIX objects remains challenging. Large language models (LLMs) often succeed at extracting low-level indicators but struggle with higher-level abstractions, leading to missing fields, invalid properties, and structurally inconsistent outputs. To address these issues, we propose a methodology that integrates instruction fine-tuning with a novel evaluation framework. Specifically, we fine-tune LLMs using curated text–STIX pairs and domain-specific instructions to internalize schema alignment and reduce hallucinations. We further introduce the Object and Properties Similarity Evaluation (OPSE), which measures both structural validity and semantic fidelity of generated STIX objects against expert ground truth. Experimental results show that our fine-tuned model substantially improves object coverage, property completeness, and structural accuracy compared with baseline prompting and existing STIX generation tools.

Next Generation Access Control (NGAC) is a standard for implementing dynamic attribute-based access control. It allows access events to trigger programmed administrative obligations and change access privileges during policy execution. However, complex obligations in an NGAC application have the potential of “grave harm to the authorization state through error or intent.” The existing work on NGAC policy testing and verification has limited effectiveness in detecting obligation errors. To address this limitation, we present a novel fault-based testing approach to determining the presence or absence of errors in NGAC policies. It hypothesizes potential errors (faults) in the given policy according to a comprehensive fault model, represents the corrected versions by policy mutants, and validates the hypotheses by generating and executing distinguishing tests. The distinguishing test of a mutant ensures that the mutant and the policy yield distinct execution results – the hypothetical error is present in the policy if the policy's execution result is wrong. We have implemented the approach based on the NGAC reference implementation and applied it to two case studies, including the first fully-fledged NGAC application with sophisticated obligations. The experiment results demonstrate that (a) the subject policies are absent from all hypothetical faults, and (b) all faulty policies represented by the mutants are revealed by fault-based tests. The results also show that the obligation tests targeting individual faults have effectively revealed multi-fault errors. Thus, the proposed approach can help detect potential errors in the development process of NGAC applications.

Machine learning has emerged as a promising method for detecting code vulnerabilities. In existing research, models trained on available samples are applied to predict potential vulnerabilities in new code within the same language. This approach may not be directly applicable when dealing with languages that have limited vulnerable samples available. This paper leverages transfer learning and k-shot tuning to address this issue, aiming to classify various Common Weakness Enumeration (CWE) categories in code written in a target language by utilizing a model trained on data from a different base language. We build upon a foundational model that enhances a state-of-the-art Graph Neural Network (GNN) framework designed for code vulnerability detection. Our experiments using extensive datasets of 42 common CWEs in C, Java, and C# have yielded valuable findings. Specifically, when models trained in one language are transferred to another, there is a noticeable improvement in detection performance. The magnitude of performance enhancements varies across different CWEs. k-shot tuning further refines the transferred models. However, the extent of performance gains gradually diminishes as the value of k increases. Once k exceeds a certain threshold, the transferred knowledge may be overwritten. Furthermore, our research unveiled an asymmetry in the two transfer learning directions within each language pair, even when the languages share the same programming paradigm. Transferred models in both directions often exhibit differing performance levels across the majority of CWEs.

Next Generation Access Control (NGAC) is a standard for implementing attribute-based access control in computer software. It allows for run-time privilege changes through administrative obligations triggered by access events. However, incorrect privilege changes due to error or intent can cause grave harm to the authorization state. It is important to ensure that the run-time privilege changes meet the access control requirements. To address this issue, we present an efficient approach to verifying NGAC policies by leveraging SMT to deal with complex policy structures and semantics. We have implemented our approach based on the NGAC reference implementation and applied it to two case studies, including the first and only fully-fledged NGAC application. We have formalized 259 access control requirements and successfully verified them against the subject policies. To further evaluate the error detection capability of our approach, we have verified 205 policy versions with a single-seeded obligation error and 154 versions with multiple-seeded obligation errors. The verification results show that all faulty policies failed to satisfy the requirements, and thus the errors were revealed.

The administrative obligation is a unique feature of Next Generation Access Control (NGAC), a standard for implementing fine-grained attribute-based access control. It provides a programming mechanism for run-time privilege changes by attaching administrative operations to authorized access events. However, dynamic privilege change raises a major concern because the application of NGAC has the potential of "grave harm to the authorization state through error or intent." It is important to reveal potential obligation errors that lead to incorrect privileges and privilege changes. To address this issue, this paper presents a family of coverage-based test generation methods for the obligations in NGAC applications. These methods can generate obligation tests to achieve the corresponding coverage criterion (obligation coverage, action coverage, decision coverage, or factor decision coverage). Each test consists of a sequence of obligation-triggering access events. We have applied the proposed methods to three NGAC applications. The experiment results demonstrate that they have different levels of fault-detection capability and cost-effectiveness.

Source code representation is critical to the machine-learning-based approach to detecting code vulnerability. This paper proposes Compact Abstract Graphs (CAGs) of source code in different programming languages for predicting a broad range of code vulnerabilities with Graph Neural Network (GNN) models. CAGs make the source code representation aligned with the task of vulnerability classification and reduce the graph size to accelerate model training with minimum impact on the prediction performance. We have applied CAGs to six GNN models and large Java/C datasets with 114 vulnerability types in Java programs and 106 vulnerability types in C programs. The experiment results show that the GNN models have performed well, with accuracy ranging from 94.7% to 96.3% on the Java dataset and from 91.6% to 93.2% on the C dataset. The resultant GNN models have achieved promising performance when applied to more than 2,500 vulnerabilities collected from real-world software projects. The results also show that using CAGs for GNN models is significantly better than ASTs, CFGs (Control Flow Graphs), and PDGs (Program Dependence Graphs). A comparative study has demonstrated that the CAG-based GNN models can outperform the existing methods for machine learning-based vulnerability detection.

This paper presents a systematic approach to designing a series of digital forensics instructional materials to address the severe shortage of active learning materials in the digital forensics community. The materials include real-world scenario-based case studies, a set of hands-on problem-driven labs for each case study, and an integrated forensic investigation environment. In this paper, we first clarify some fundamental concepts related to digital forensics, such as digital forensic artifacts, artifact generators, and evidence. We then re-categorize knowledge units of digital forensics based on the artifact generators for measuring the coverage of learning outcomes and topics. Finally, we utilize a real-world cybercrime scenario to demonstrate how knowledge units, digital forensics topics, concepts, artifacts, and investigation tools can be infused into each lab through active learning. The repository of the instructional materials is publicly available on GitHub. It has gained nearly 600 stars and 22k views within several months.

Making digital evidence presentable is hard due to the intangible and complex nature of digital evidence and the variety of targeted audiences. In this paper, we present Digital Forensic Knowledge Graph (DFKG) for visualizing and reasoning about digital forensic evidence. We first describe the criteria of presentable evidence to ensure authenticity, integrity, validity, credibility, and relevance of evidence. Then we specify DFKG to capture presentable forensic evidence from three perspectives: (1) the background of a criminal case, (2) the reconstructed timeline of a criminal case, and (3) the verifiable digital evidence related to the criminal activity timeline. We also present a case study to illustrate the DFKG-based approach.

Policy testing is an important means for quality assurance of access control policies. Experimental studies on the testing methods of XACML policies have shown their varying levels of effectiveness. However, there is a lack of explanation for why they are unable to detect certain types of faults. It is unclear what is essential to the fault detection capability. To address this issue, we propose a theory on policy testing by formalizing the fault detection conditions with respect to a comprehensive fault model of XACML policies. The detection condition of a policy fault, composed of the reachability, necessity, and propagation constraints, is sufficient and necessary for revealing the fault. The formalized fault detection conditions can qualify the inherent strengths and limitations of testing methods. We have applied the formalization to the qualitative evaluations of five testing methods for the current version of the XACML standard. The results show that, for each method, there are certain types of faults that can always or never be revealed, while the detection of other faults may depend on the particular policy structure.

As the pioneer of blockchain technology, Bitcoin is the most famous cryptocurrency to date. Given its dramatic price swings along with constant news and events, the dynamics of cryptocurrencies are difficult to quantify. These dynamics are believed to be affected by various political, security, financial, and regulatory events. This paper presents the Impact-Score metric, an efficient framework that attempts to quantify the impact of events on the Bitcoin blockchain. We have applied our framework to 16 major worldwide events and the Bitcoin blockchain network (defined as Bitcoin transaction and users, blockchain data, and memory pool data) from 2016-2018. The results show that the majority of the events are correlated with quantifiable changes in the Bitcoin blockchain and network. We also observed correlations between event types (e.g. financial events) and event subtypes on certain Bitcoin blockchain network temporal features.

Integer overflow is a common cause of software failure and security vulnerability. Existing approaches to detecting integer overflow errors rely on traditional static code analysis and dynamic testing. This paper presents a novel machine learning-based approach that predicts integer overflow errors by treating source code as text. It exploits text classifiers to determine whether each method in a given Java program contains an integer overflow error. As the training data is essential, we have constructed a comprehensive dataset to accounts for (a) integer overflow errors of all integer types and operations in Java (i.e., positive samples); (b) various programming techniques for preventing integer overflow errors (i.e., negative samples); and (c) malicious scenarios that may mislead text classifiers (i.e., adversarial samples). We have trained three classifiers, BERT, fastText, and NBSVM, that represent different text embedding techniques. BERT, as a representative deep-learning transformer, has achieved the highest performance scores and remained robust even when tested with the adversarial samples.

The NGAC (Next Generation Access Control) standard for attribute-based access control (ABAC) allows for run-time changes of the permission and prohibition configurations through administrative obligations triggered by access events. It makes access control more fine-grained and dynamic. However, it raises challenges for assuring the correctness of NGAC policies. As policy testing is an important technique for quality assurance, this paper presents an approach to mutation analysis of NGAC policies. It can evaluate the effectiveness of a testing method and reveal potential faults in an inadequately tested policy. The mutation analysis covers various types of potential faults in the assignments, associations, prohibitions, and obligations of NGAC policies. This paper also proposes an incremental testing approach that first validates the initial configuration of a policy and then the policy as a whole. It helps determine whether faults appear in the configuration or the obligations. To evaluate the work, we have developed four working policies and their test suites based on the current NGAC reference implementation. The empirical studies show that the mutation analysis can shed light on the strengths and weaknesses of the test suites. They also demonstrate the need for developing more cost-effective testing methods.

While the decoupling of control and data planes in software-defined networking (SDN) facilitates orchestrating network traffic, it suffers from security threats. For example, saturation attacks can make SDN out of service by exhausting the controller' and switch's computational resources. The existing research has focused on defense against limited types of saturation attacks. In this paper, we propose vSwitchGuard, a framework for detection and countermeasure of known and unknown saturation attacks in SDN. vSwitchGuard aims to identify the victim switches targeted by known or unknown types of saturation attacks with machine learning classifiers and restore the victim switches to their safe state through deep packet inspection. We have evaluated three supervised classifiers and four semi-supervised classifiers for five types of saturation attacks (TCP-SYN, UDP, ICMP, IP-Spoofing, and TCP-SARFU) and their combinations. The results suggest that supervised and semi-supervised classifiers can be combined to deal with known and unknown attacks for better performance. We have also implemented the countermeasure and evaluated it with all combinations of the five types of attacks. The results demonstrate that vSwitchGuard can effectively defend against the attacks without significant performance overhead.

Expanding abbreviations in source code to their full meanings is very useful for software maintainers to comprehend the source code. The existing approaches, however, focus on expanding an abbreviation to a single word, i.e., unigram. They do not perform well when dealing with abbreviations of phrases that consist of multiple unigrams. This paper proposes a bigram-based approach for retrieving abbreviated phrases automatically. Key to this approach is a bigram-based inference model for choosing the best phrase from all candidates. It utilizes the statistical properties of unigrams and bigrams as prior knowledge and a bigram language model for estimating the likelihood of each candidate phrase of a given abbreviation. We have applied the bigram-based approach to 100 phrase abbreviations, randomly selected from eight open source projects. The experiment results show that it has correctly retrieved 78% of the abbreviations by using the unigram and bigram properties of a source code repository. This is 9% more accurate than the unigram-based approach and much better than other existing approaches. The bigram-based approach is also less biased towards specific phrase sizes than the unigram-based approach.

While the existing methods for testing XACML policies have varying levels of effectiveness, none of them can reveal the majority of policy faults. The undisclosed faults may lead to unauthorized access and denial of service. This paper presents an approach to strong mutation testing of XACML policies that automatically generates tests from the mutants of a given policy. Such mutants represent the targeted faults that may appear in the policy. In this approach, we first compose the strong mutation constraints that capture the semantic difference between each mutant and its original policy. Then, we use a constraint solver to derive an access request (i.e., test). The test suite generated from all the mutants of a policy can achieve a perfect mutation score, thus uncover all hypothesized faults or demonstrate their absence. Based on the mutation-based approach, this paper further explores optimal test suite that achieves a perfect mutation score without duplicate tests. To evaluate the proposed approach, our experiments have included all the subject policies in the relevant literature and used a number of new policies. The results demonstrate that: (1) it is scalable to generate a mutation-based test suite to achieve a perfect mutation score, (2) it can be impractical to generate the optimal test suite due to the expensive removal of duplicate tests, (3) different from the results of the existing study, the modified-condition/decision coverage-based method, currently the most effective one, has low mutation scores for several policies.

As a new networking paradigm, Software-Defined Networking (SDN) separates data and control planes to facilitate programmable functions and improve the efficiency of packet delivery. Recent studies have shown that there exist various security threats in SDN. For example, a saturation attack may disturb the normal delivery of packets and even make the SDN system out of service by flooding the data plane, the control plane, or both. The existing research has focused on saturation attacks caused by SYN flooding. This paper presents an anomaly detection method, called SA-Detector, for dealing with a family of saturation attacks through IP spoofing, ICMP flooding, UDP flooding, and other types of TCP flooding, in addition to SYN flooding. SA-Detector builds upon the study of self-similarity characteristics of OpenFlow traffic between the control and data planes. Our work has shown that the normal and abnormal traffic flows through the OpenFlow communication channel have different statistical properties. Specifically, normal OpenFlow traffic has a low self-similarity degree whereas the occurrences of saturation attacks typically imply a higher degree of self-similarity. Therefore, SA-Detector exploits statistical results and self-similarity degrees of OpenFlow traffic, measured by Hurst exponents, for anomaly detection. We have evaluated our approach in both physical and simulation SDN environments with various time intervals, network topologies and applications, Internet protocols, and traffic generation tools. For the physical SDN environment, the average accuracy of detection is 97.68% and the average precision is 94.67%. For the simulation environment, the average accuracy is 96.54% and the average precision is 92.06%. In addition, we have compared SA-Detector with the existing saturation attack detection methods in terms of the aforementioned performance metrics and controller's CPU utilization. The experiment results indicate that SA-Detector is effective for the detection of saturation attacks in SDN.

Bitcoin [1] as a popular digital currency has been a target of theft and other illegal activities. Key to the forensic investigation is to identify bitcoin addresses involved in bitcoin transfers. This paper presents a framework, FABT, for forensic analysis of bitcoin transactions by identifying suspicious bitcoin addresses. It formalizes the clues of a given case as transaction patterns defined over a comprehensive set of features. FABT converts the bitcoin transaction data into a formal model, called Bitcoin Transaction Net (BTN). The traverse of all bitcoin transactions in the order of their occurrences is captured by the firing sequence of all transitions in the BTN. We have applied FABT to identify suspicious addresses in the Mt.Gox case. A subgroup of the suspicious addresses has been found to share many characteristics about the received/transferred amount, number of transactions, and time intervals.

In order to study the variation law of the influence degree of air quality factors under time series, this article selects the hourly concentration values of NO2and O3from November 2017 to October 2018 in Lanzhou city as the research object, and based on the coarse granulation method, NO2and O3. The correlation value of hourly concentration value is transformed into the influence degree symbol, and the sequence of effect degree variation under time series is obtained. The network model is constructed by using complex network theory to analyze the time series of NO2and O3influence degree series, and the differences and changes in network topology characteristics in overall and different season effect degree symbols of Lanzhou are analyzed. The results show the following. First, from the network analysis, the number of negative correlations of NO2to O3is far greater than that of positive correlation and basic noncorrelation effect degree, indicating that NO2and O3are negatively correlated. From the factor of season, the law of negative correlation is summer > autumn > spring > winter, indicating that light and temperature are the main factors for the conversion of NO2to O3. Second, through the analysis of Lanzhou's overall and seasonal related network topological features, such as node degree distribution, node intensity distribution, and network betweenness, the change sequence consisting of the influence degree symbols h, H, and m plays an important role in each network. The sequence of changes consisting of M, H, and S has the lowest effect in each network, indicating that in the day of the time series, the conversion of NO2to O3in Lanzhou is mainly dominated by different degrees of negative correlation. Third, through the analysis of network cluster degree, it is found that most of the changes in the degree of change have a transformation and a high degree of transformation, indicating that the effect of NO2on O3in the original sequence is less stable. Fourth, through the network average shortest path and diameter analysis, it is found that the conversion between the changes in the degree of influence requires at least one day and at most three days. That is to say, the influence of NO2on O3can be maintained for up to three days. From the network, the complexity of the influence of NO2on O3in the original sequence of four seasons was founded.

With the increasing inter-connection of operation technology to the IT network, the security threat to the Industrial Control System (ICS) is increasing daily. Therefore, it is critical to utilize formal verification technique such as model checking to mathematically prove the correctness of security and safety requirements in the controller logic before it is deployed on the field. However, model checking requires considerable effort for regular ICS users and control technician to verify properties. This paper, provides a simpler approach to the model checking of temperature process control system by first starting with the control module design without formal verification. Second, identifying possible vulnerabilities in such design. Third, verifying the safety and security properties with a formal method.

In LinkedIn, skill endorsements are used as a key indicator to assess a user's skill level so that a recruiter can find right candidates. However, the simple counting of skill endorsements has shown serious limitations to correctly assess a user's skill level particularly when false endorsements prevail for self-promotion or collusive promotion. To address this issue, we propose a framework using regression analysis to evaluate assessment methods under varying the degree of false endorsements. We define two types of assessment scores: authority score (AS) and credit score (CS). The AS is calculated based on an endorser's expertise level in a particular skill set while the CS is estimated based on the endorser's trustworthiness. Based on these two types of skill assessments, we define a hybrid method that calculates AS based on CS, which is called credit-based AS, or namely CAS. We conduct performance analysis by comparing the AS and CAS with the endorsement count (EC) as a baseline model, which is currently used in LinkedIn. Through the extensive regression analysis, under varying the degree of false endorsements from 10% to 25%, we observe that the CAS outperforms AS and EC with less than 10% of false endorsements. On the other hand, the AS performs the best among three methods with 10%-25% of false endorsements. Based on the regression analysis of the skillset assessment framework, the real dataset collected for this study is likely to have 4%-6% of false endorsements. This finding implies that an endorser's expertise appears more critical than the endorser's trustworthiness under more presence of false endorsements because the unqualified endorser's endorsement may not be necessarily true.

Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.

Software-Defined Networking (SDN) is a new net-working paradigm that has revolutionized network architectures. The separation of data and control planes improves the efficiency of packet delivery. However, there exist various security attacks against SDN systems. For example, a saturation attack may disturb the normal delivery of packets and even make the SDN system out of service by flooding the data plane, the control plane, or both. This paper presents an anomaly detection method, called SA-Detector, for dealing with a family of saturation attacks. SA-Detector builds upon the study of self-similarity of OpenFlow traffic, which has shown that the normal and abnormal traffic patterns between the controller and the OpenFlow switches have different characteristics. We have evaluated the performance of SA-Detector with different time scales, network scales, Internet applications, and attack implementations. The experimental results show that the average accuracy is 96.54% and the average precision is 92.06%. This indicates that SA-Detector is effective for detecting saturation attacks.

Attribute-based access control (ABAC) with obligations is a new technique for achieving fine-grained access control and accountability. An obligatory ABAC system can be implemented incorrectly for various reasons, such as programming errors and incorrect access control and obligation specification. To reveal these implementation defects, this paper presents an approach to model-based testing of obligatory ABAC systems. In this approach, we first build a test model by specifying a functional model and an obligatory ABAC policy. The policy represents access control and obligation constraints on the functional model. Then we weave the policy with the functional model into an integrated model that represents both functions under test and access control and obligation constraints on them. Test cases can then be generated from the integrated model. Our approach is built upon MISTA, an open source test code generator that supports a variety of programming languages and test frameworks. To validate our approach, this paper presents a first case study on the development and testing of an open-source obligatory ABAC system. We evaluated the effectiveness of the approach by mutation analysis of the ABAC and obligation rules and the policy enforcement code in the implementation. The result shows that our approach is capable of finding the majority of injected faults.

While the standard language XACML is very expressive for specifying fine-grained access control policies, defects can get into XACML policies for various reasons, such as misunderstanding of access control requirements, omissions, and coding errors. These defects may result in unauthorized accesses, escalation of privileges, and denial of service. Therefore, quality assurance of XACML policies for real-world information systems has become an important issue. To address this issue, this paper presents a family of coverage criteria for XACML policies, such as rule coverage, rule pair coverage, decision coverage, and Modified Condition/Decision Coverage (MC/DC). To demonstrate the assurance levels of these coverage criteria, we have developed methods for automatically generating tests, i.e., access requests, to satisfy the coverage criteria using a constraint solver. We have evaluated these methods through mutation analysis of various policies with different levels of complexity. The experiment results have shown that the rule coverage is far from adequate for revealing the majority of defects in XACML policies, and that both MC/DC and decision coverage tests have outperformed the existing methods for testing XACML policies. In particular, MC/DC tests achieve a very high level of quality assurance of XACML policies.

This paper presents XPA (XACML Policy Analyzer), an open source IDE (Integrated Development Environment) for testing, debugging, and mutating XACML 3.0 policies.XACML is an OASIS standard for specifying attributebased access control policies.XPA provides a variety of new techniques for generating test cases from policies, localizing bugs in faulty policies, and repairing faulty policy elements.XPA has been applied to numerous XACML policies from the literature and real-world applications.These policies have been used to quantitatively evaluate the effectiveness of various testing and debugging methods.For system developers and administrators, XPA is a practical IDE for developing dependable XACML policies.For access control researchers, XPA offers a versatile toolkit for studying and evaluating new testing, debugging, and verification techniques.

Effective friend classification in Online Social Networks (OSN) has many benefits in privacy. Anything posted by a user in social networks like Facebook is distributed among all their friends. Although the user can select the manual option for their post-dissemination, it is not feasible every time. Since not all friends are the same in social networks, the visibility access for the post should be different for different strengths of friendship for privacy. Previous works in finding friendship strength in social networks have used interaction and similarity based features but none of them has considered using sentiment-based features as the driving factor to determine the strength.

Source code readability is critical to software quality assurance and maintenance. In this paper, we present a novel approach to the automated measurement of source code readability based on Word Concreteness and Memory Retention (WCMR) of variable names. The approach considers programming and maintenance as processes of organizing variables and their operations to describe solutions to specific problems. The overall readability of given source code is calculated from the readability of all variables contained in the source code. The readability of each variable is determined by how easily its meaning is memorized (i.e., word concreteness) and how quickly they are forgotten over time (i.e., memory retention). Our empirical study has used 14 open source applications with over a half-million lines of code and 10,000 warning defects. The result shows that the WCMR-based source code readability negatively correlates strongly with overall warning defect rates, and particularly with such warning as bad programming practices, code vulnerability, and correctness bug warning.

Programmers often utilize abbreviations for naming identifiers when writing code. However, the difficulty to retrieve the original words of abbreviations during the maintenance phase makes the source code more problematic to comprehend. In this paper, we describe a Bayesian unigram-based inference to automatically expand abbreviations to their original words to enhance source code comprehension. Our approach automatically extracts a list of candidate words from the source code for a given abbreviation and employs the abbreviation's unigram statistical properties as evidence to find the best candidate word. We evaluated our approach on a set of 531 abbreviations randomly picked from eight open source projects and found that our approach correctly expands 83.62% of the set. Our approach provides an improvement of 48.3% in abbreviation expansion accuracy over the current state-of-the-art approaches.

Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.

In online social networks (OSNs), individual users have a strong desire to expand their social networks through OSN activities and try to maximize the benefits from the social relationships, called social capital. However, with a large-scale social network, their privacy rights have been significantly intruded by adversarial users that perform social attacks including false / illegal private information dissemination or the use of fake identities. In this work, we study how individual users can expand their social networks by making trustworthy friends while not leaking their private information out to unauthorized parties or social attackers. We adopt the concepts of trust and reputation in order to preserve users' privacy while enhancing their social capital in OSNs. Given a social network topology from the Facebook, we model an individual user's interactions with other users based on feeding (e.g., posting information) and feedback behaviors (e.g., providing likes or comments). Our results show that there exists a tradeoff between social capital and privacy preservation. In addition, we show there exists a balance point of social capital and privacy thresholds that maximizes correct information diffusion while minimizing illegal private information leakout, given users' risk appetite for preserving privacy.

Due to the proliferation of using various online social media, individual users put their privacy at risk by posting and exchanging enormous amounts of messages or activities with other users. This causes a serious concern about leaking private information out to malevolent entities without users’ consent. This work proposes a reputation model in order to achieve efficient and effective privacy preservation in which a user’s reputation score can be used to set the level of privacy and accordingly to determine the level of visibility for all messages or activities posted by the users. We derive a user’s reputation based on both individual and relational characteristics in online social network environments. We demonstrate how the proposed reputation model can be used for automatic privacy assessment and accordingly visibility setting for messages / activities created by a user.

Access control policies written in the XACML standard language tend to be complex due to the great variety of attribute types and operations for fine-grained access control. The complexity not only increases the likelihood of having authorization faults in access control policies, but also makes it challenging to find and fix these faults. This paper presents an approach for automating the process of debugging XACML policies. It consists of two main techniques: fault localization and mutation-based policy repair. Fault localization aims to find the most suspicious policy elements according to the correlation between the execution information of policy elements and the test execution results. Mutation-based policy repair aims to modify the suspicious policy elements by using well-defined mutation operators. Our empirical studies have used a large number of faulty policies with one or two seeded faults. Our approach was able to repair all of them automatically. We have also compared several scoring methods for ranking suspicious policy elements. The results show that Naish2 and CBI-Inc are very efficient for automatic repair.

Access control policies in distributed systems, particularly implemented in the XACML standard language, are increasingly complex. Faults may exist in complex policies for various reasons such as misunderstanding of the access control requirements, omissions, and coding errors. These faults, if not removed before deployment, may lead to unauthorized accesses or denial of service. Manual localization of these faults, however, can be a challenging task. Inspired by spectrum-based fault localization for software debugging, this paper presents an approach for automatically localizing the fault(s) in a given XACML policy by exploring test coverage information of the policy elements. We investigate two test coverage criteria (i.e., reachability and firing) of policy elements and 14 scoring methods for ranking policy elements to determine the fault location(s). To evaluate the fault localization methods, we have used real-world policy files with different levels of complexity and a large number of policy mutants with one or two seeded faults. The experiment results show that the firing-based Naish2 and CBI-Inc methods are effective in fault localization of XACML policies.

As a new generation access control method, Attribute-Based Access Control (ABAC) has gained increasing attention.Currently, Balana is the only open-source implementations of XACML 3.0, which is an OASIS standard for specifying ABAC.Considering that XACML is much more complex than traditional access control models, conformance testing of any XACML implementation is an important problem.Using a non-conformance implementation may lead to misunderstanding of access decisions or even security violations.This paper presents an approach to conformance testing of Balana, focusing on the main elements of the XACML3.0language, such as targets, rules, policies, and policy sets.In particular, we have thoroughly tested the key rule combining algorithms in policies and policy combining algorithms in policy sets.This has revealed several conformance issues.

Modern computer software usually consists of a number of interacting components. Defects pertaining to component interactions may not be visible until the components are integrated. To exercise component interactions, we propose an integration testing approach based on the core concept of contracts (i.e., preconditions and postconditions of component calls in first-order logic). To enable correctness analysis and generation of coverage-based tests (including state coverage, transition or component coverage, and reachability coverage) of a contract-based test model, we transform the test model into an operational model. We have implemented this approach into a framework that has the capacity to generate executable test code in a large collection of programming languages and to run the generated test code in a rich variety of test execution environments. To demonstrate the cost-effectiveness of our approach, we have conducted a series of experiments in controlled environments to measure the performance of test generation and the fault detection capabilities of coverage-based tests. The results have clearly demonstrated that: 1) our approach can quickly generate coverage-based tests when there is enough memory for dealing with the state space of the given test models; 2) reachability coverage is more capable of detecting faults than state coverage and transition coverage; 3) postcondition-based test oracles are more capable of detecting faults than state-based test oracles; and 4) robustness tests, which exercise the situations when the contracts are broken, are important for improving fault detection capability.

Presents a listing of the Symposium organizing committee.

XACML is a standard language for specifying attribute-based access control policies of computer and software systems. It offers a variety of combining algorithms for flexible policy composition. While they are intended to be different, they also bear similarities. Some combining algorithms can be functionally equivalent with respect to the given policy or policies. To correctly use the combining algorithms, it is important to understand the subtle similarities and differences. This paper presents a formal treatment of the semantic differences between the commonly used combining algorithms in XACML 3.0. For each pair of the selected combining algorithms, we identify when they are functionally equivalent and when they are not equivalent. This rigorous understanding helps minimize incorrect uses of combining algorithms that may lead to unauthorized access and denial of service. It also provides a foundation for determining equivalent mutants of combining algorithms in mutation testing of XACML policies.

With the increasing complexity of software, new access control methods have emerged to deal with attributebased authorization.As a standard language for attribute-based access control policies, XACML offers a number of rule and policy combining algorithms to meet different needs of policy composition.Due to their variety and complexity, however, it is not uncommon to apply combining algorithms incorrectly, which can lead to unauthorized access or denial of service.To solve this problem, this paper presents a fault-based testing approach for determining incorrect combining algorithms in XACML 3.0 policies.It exploits an efficient constraint solver to generate queries to which a given policy produces different responses than its combining algorithm-based mutants.Such queries can determine whether or not the given combining algorithm is used correctly.Our empirical studies using sizable XACML policies have demonstrated that our approach is effective.

With the increasing complexity of software, new access control methods have emerged to deal with attribute-based authorization. As a standard language for specifying attribute-based access control policies, XACML offers a number of rule and policy combining algorithms to meet different needs of policy composition. Due to their variety and complexity, however, it is not uncommon to apply combining algorithms incorrectly, which can lead to unauthorized access or denial of service. To solve this problem, this paper presents a fault-based testing approach for revealing incorrect combining algorithms in XACML 3.0 policies. The theoretical foundation of this approach relies on the formalization of semantic differences between rule combining algorithms and between policy combining algorithms. It allows the use of a constraint solver for generating queries to which a given policy produces different responses than its combining algorithm-based mutants. Such queries can determine whether or not the given combining algorithm is used correctly. Our empirical studies using various XACML policies have demonstrated that our approach is effective.

Role-based access control is an important access control method for securing computer systems. A role-based access control policy can be implemented incorrectly due to various reasons, such as programming errors. Defects in the implementation may lead to unauthorized access and security breaches. To reveal access control defects, this paper presents a model-based approach to automated generation of executable access control tests using predicate/transition nets. Role-permission test models are built by integrating declarative access control rules with functional test models or contracts (preconditions and postconditions) of the associated activities (the system functions). The access control tests are generated automatically from the test models to exercise the interactions of access control activities. They are transformed into executable code through a model-implementation mapping that maps the modeling elements to implementation constructs. The approach has been implemented in an industry-adopted test automation framework that supports the generation of test code in a variety of languages. The full model-based testing process has been applied to three systems implemented in Java. The effectiveness is evaluated through mutation analysis of role-based access control rules. The experiments show that the model-based approach is highly effective in detecting the seeded access control defects.

The world's increased dependence on software-enabled systems has raised major concerns about software reliability and security. New cost-effective tools for software quality assurance are needed. This paper presents an automated test generation technique, called Model-based Integration and System Test Automation (MISTA), for integrated functional and security testing of software systems. Given a Model-Implementation Description (MID) specification, MISTA generates test code that can be executed immediately with the implementation under test. The MID specification uses a high-level Petri net to capture both control- and data-related requirements for functional testing, access control testing, or penetration testing with threat models. After generating test cases from the test model according to a given criterion, MISTA converts the test cases into executable test code by mapping model-level elements into implementation-level constructs. MISTA has implemented test generators for various test coverage criteria of test models, code generators for various programming and scripting languages, and test execution environments such as Java, C, C++, C#, HTML-Selenium IDE, and Robot Framework. MISTA has been applied to the functional and security testing of various real-world software systems. Our experiments have demonstrated that MISTA can be highly effective in fault detection.

Search-based test generation can automatically produce a large volume of test inputs. However, it is difficult to define the test oracle for each of the test inputs. This paper presents a mining approach to building a decision tree model according to the test inputs generated from Java bytecode. It converts Java bytecode into the Jimple representation, extracts predicates from the control flow graph of the Jimple code, and uses these predicates as attributes for organizing training data to build a decision tree. Our case studies show that the mining approach generated accurate behavioral models and that test oracles derived from these models were able to kill 94.67% of the mutants with injected faults.

This paper presents a unique summer project for a group of undergraduate students and high school computer teachers to gain research experiences in the area of cybersecurity. The students and teachers were selected from the participants in the NSF REU and RET programs at the host institution. Through the research on security testing of a real-world online banking system, the students and teachers have not only learned about the cutting-edge security testing techniques, but also made publishable contributions to the research base. The two collaborating graduate assistants served as an immediate role model for the undergraduates and an indirect role model for high school students through the teachers. With the help from the graduate assistants, the students and teachers were able to work effectively toward achieving their research objectives. The internal competition helped the participants get a better sense of achievement and satisfaction. The research experiences also prepared the teachers with the necessary knowledge for introducing cybersecurity topics (e.g., secure programming) into future classroom activity. As such, the project described in this paper provides a model summer program for undergraduate and/or K-12 teachers to gain research experiences.

SUMMARY Software security issues have been a major concern in the cyberspace community, so a great deal of research on security testing has been performed, and various security testing techniques have been developed. Threat modeling provides a systematic way to identify threats that might compromise security, and it has been a well‐accepted practice by the industry, but test case generation from threat models has not been addressed yet. Thus, in this paper, we propose a threat model‐based security testing approach that automatically generates security test sequences from threat trees and transforms them into executable tests. The security testing approach we consider consists of three activities in large: building threat models with threat trees; generating security test sequences from threat trees; and creating executable test cases by considering valid and invalid inputs. To support our approach, we implemented security test generation techniques, and we also conducted an empirical study to assess the effectiveness of our approach. The results of our study show that our threat tree‐based approach is effective in exposing vulnerabilities. Copyright © 2012 John Wiley & Sons, Ltd.

Building effective test models is critical to the applications of model-based testing. This paper presents a methodology for guiding model-based testing with function nets, which are lightweight high-level Petri nets. High-level Petri nets are traditionally used for modeling, simulation, and verification purposes. In this paper, however, function nets are test models for automated generation of test cases. The proposed methodology has three key features. First, based on an analogy between modeling and programming, it identifies the basic building blocks for composing test models. Second, it provides structured processes for building test models from workflows and from the contracts of the components under test. Third, it provides several techniques for reducing the complexity of test models and thus the number of tests. The methodology has been applied to the function testing and security testing of several industry-strength applications.

Access control policies in software systems can be implemented incorrectly for various reasons. This paper presents a model-based approach for automated testing of access control implementation. To feed the model-based testing process, test models are constructed by integrating declarative access control rules and contracts (preconditions and post-conditions) of the associated activities. The access control tests are generated from the test models to exercise the interactions of access control activities. Test executability is obtained through a mapping of the modeling elements to implementation constructs. The approach has been implemented in an industry-adopted test automation framework that supports the generation of test code in a variety of languages, such as Java, C, C++, C#, and HTML/Selenium IDE. The full model-based testing process has been applied to two systems implemented in Java. The effectiveness is evaluated in terms of access-control fault detection rate using mutation analysis of access control implementation. The experiments show that the model-based tests killed 99.7% of the mutants and the remaining mutants caused no policy violations.

SUMMARY Aspect‐oriented programming yields new types of programming faults due to the introduction of new constructs for dealing with crosscutting concerns. To reveal aspect faults, this paper presents a framework for testing whether or not aspect‐oriented programs conform to their state models. It supports two families of strategies (i.e. structure‐oriented and property‐oriented) for automated generation of aspect tests from aspect‐oriented state models. A structure‐oriented testing strategy derives tests and test code from an aspect‐oriented state model to meet a given structural coverage criterion, such as state coverage, transition coverage, or round trip. A property‐oriented testing strategy generates test code from the counterexamples of model checking. Two such strategies are checking an aspect‐oriented state model against trap properties and checking mutants of aspect models against system properties. Mutation analysis of aspect‐oriented programs is used to evaluate the effectiveness of these testing strategies. The experiments demonstrate that testing aspect‐oriented programs against their state models can detect many aspect faults. The comparative evaluations also reveal that the structure‐oriented and property‐oriented testing strategies complement each other—some aspect faults were detected by the structure‐oriented strategies, but not by the property‐oriented strategies and vice versa. Copyright © 2010 John Wiley & Sons, Ltd.

Security attacks typically result from unintended behaviors or invalid inputs. Security testing is labor intensive because a real-world program usually has too many invalid inputs. It is highly desirable to automate or partially automate security-testing process. This paper presents an approach to automated generation of security tests by using formal threat models represented as Predicate/Transition nets. It generates all attack paths, i.e., security tests, from a threat model and converts them into executable test code according to the given Model-Implementation Mapping (MIM) specification. We have applied this approach to two real-world systems, Magento (a web-based shopping system being used by many online stores) and FileZilla Server (a popular FTP server implementation in C++). Threat models are built systematically by examining all potential STRIDE (spoofing identity, tampering with data, repudiation, information disclosure, denial of service, and elevation of privilege) threats to system functions. The security tests generated from these models have found multiple security risks in each system. The test code for most of the security tests can be generated and executed automatically. To further evaluate the vulnerability detection capability of the testing approach, the security tests have been applied to a number of security mutants where vulnerabilities are injected deliberately. The mutants are created according to the common vulnerabilities in C++ and web applications. Our experiments show that the security tests have killed the majority of the mutants.

It is becoming prohibitively expensive and time consuming, as well as tedious and error-prone, to perform debugging manually. Among the debugging activities, fault localization has been one of the most expensive, and therefore, a large number of fault-localization techniques have been proposed over the recent years. This paper presents a crosstab-based statistical technique that makes use of the coverage information of each executable statement and the execution result (success or failure) with respect to each test case to localize faults in an effective and efficient manner. A crosstab is constructed for each executable statement, and a statistic is computed to determine the suspiciousness of the corresponding statement. Statements with a higher suspiciousness are more likely to contain bugs and should be examined before those with a lower suspiciousness. Case studies are performed on both small- (the Siemens and Unix suites) and large-sized programs (space, grep, gzip, and make), and results suggest that the crosstab-based technique (CBT) is more effective (in terms of a smaller percentage of executable statements that have to be examined until the first statement containing the fault is reached) than other techniques, such as Tarantula. Further studies using the Siemens suite reveal that the proposed technique is also more effective at locating faults than other statistically oriented techniques, such as SOBER and Liblit05. Additional experiments evaluate the CBT from other perspectives, such as its efficiency in terms of time taken, its applicability to object-oriented languages (on a very large Java program: Ant), and its sensitivity to test suite size, and demonstrate its superior performance.

Availability is an important issue in distributed systems providing quality of services. Data or service availability modeling is very important to ensure such quality of services. Many factors, such as node availability and network link availability, could affect the data or service availability in a distributed system, and replication schemes have been widely used to improve data or service availability. In this paper, we consider node and network link failures, as well as the impact of multiple replicas on data availability. Efficient availability computing algorithms are developed to model data availability for a system with different topologies. Finally, experimental studies have been conducted to see how well our modeling approach is for the availability modeling of distributed environment with data replication.

Functional modeling and safety analysis are two important aspects of safety-critical embedded systems. However, they are often conducted separately. In this paper, we present an approach for integrating fault-tree-based safety analysis into statechart-based functional modeling. The proposed approach uses systematic transformation steps that maintain the semantics of both the fault tree and the statechart. It also provides a set of conversion rules that transform the gates of fault trees into statechart notations. The resultant model shows how the system behaves when a failure condition occurs and acts as a basis model that ensures safety through requirement validation. Using the gas burner case study, we demonstrate the advantages of the integrated model over the use of separate models, such as the lack of ambiguities, separation of concerns, and taking the order of the occurrence of faults into consideration.

In aspect-oriented programming, aspects are essentially incremental modifications to their base classes. Therefore aspect-oriented programs can be tested in an incremental fashion - we can first test the base classes and then test the base classes and aspects as a whole. This paper demonstrates that, in this incremental testing paradigm, we can prioritize aspect tests so as to report failure earlier. We explore test prioritization for testing aspect-oriented programs against their state models with transition coverage and round-trip coverage. Aspect tests are generated from woven state models obtained by composing aspect models into their base class models. We prioritize aspect tests by identifying the extent to which an aspect modifies its base classes. The modification is measured by the number of new and changed components in state transitions (start state, event, precondition, postcondition, end state). Transitions with more changes have higher priorities for test generation. We evaluate the impact of aspect test prioritization through mutation analysis of two AspectJ programs, where all aspects and their base classes can be modeled by finite state machines. We create aspect mutants of each AspectJ program according to a comprehensive AspectJ fault model. Then we test each mutant with the test suites generated without prioritization and with prioritization, respectively. Our experiment results show that prioritization of aspect tests has accelerated failure report.

Poor design has been a major source of software security problems. Rigorous and designer-friendly methodologies for modeling and analyzing secure software are highly desirable. A formal method for software development, however, often suffers from a gap between the rigidity of the method and the informal nature of system requirements. To narrow this gap, this paper presents a UML-based framework for modeling and analyzing security threats (i.e. potential security attacks) rigorously and visually. We model the intended functions of a software application with UML statechart diagrams and the security threats with sequence diagrams, respectively. Statechart diagrams are automatically converted into a graph transformation system, which has a well-established theoretical foundation. Method invocations in a sequence diagram of a security threat are interpreted as a sequence of paired graph transformations. Therefore, the analysis of a security threat is conducted through simulating the state transitions from an initial state to a final state triggered by method invocations. In our approach, designers directly work with UML diagrams to visually model system behaviors and security threats while threats can still be rigorously analyzed based on graph transformation.

This paper presents an approach to automated generation of executable test code from class models represented by the UML protocol state machines. It supports several coverage criteria for state models, including state coverage, transition coverage, and basic and extended round-trip coverage. It allows the tester to add and modify detailed test parameters (e.g., actual arguments for method invocations and implementation-specific environments) if necessary. When the state model is modified due to requirements change, the hand-crafted test parameters, if still valid, are automatically reused. This reduces the working load for regeneration of tests for modified models. In addition to test code, we also automatically generate state wrapper aspects in AspectJ, which facilitates comparing actual object states to expected states during test execution. This enables the automated verdict of pass/failure for test cases without the need to modify the source code of the class under test. We present two examples for which the executable test code is generated. They demonstrate the reuse of test parameters and testing of object interactions, respectively.

As software systems are encompassing a wide range of fields and applications, software reliability becomes a crucial step. The need for safety analysis and test cases that have high probability to uncover plausible faults are necessities in proving software quality. System models that represent only the operational behavioral of a system are incomplete sources for deriving test cases and performing safety analysis before the implementation process. Therefore, a system model that encompasses faults is required. This paper presents a technique that formalizes a safety model through the incorporation of faults with system specifications. The technique focuses on introducing semantic faults through the integration of fault trees with system specifications or statechart. The method uses a set of systematic transformation rules that tries to maintain the semantics of both fault trees and statechart representations during the transformation of fault trees into statechart notations.

A formal method for software development often introduces a gap between rigidity of the method and informal nature of system requirements. This paper presents a UML-based framework for design and analysis of dependable software while narrowing such a gap. We model the intended functions of a software application with UML statecharts and security threats, i.e., potential attacks, with sequence diagrams. The statechart diagrams are converted into a graph transformation system, which is a well-studied formal method. This allows security threats to be verified against intended functions.

The new constructs in aspect-oriented programming bring new types of programming faults with respect to crosscutting concerns, such as incorrect pointcuts and advice. This paper presents a UML-based approach to testing whether or not an aspect-oriented program conforms to its expected crosscutting behavior. We explore aspect-oriented UML design models to derive tests for exercising interactions between aspects and classes. Each aspect-oriented model consists of class diagrams, aspect diagrams, and sequence diagrams. For a method under test, we weave the sequence diagrams of the advice on the method into the method's sequence diagram. Based on the woven sequence diagram and class/aspect diagrams, we then generate an AOF (Aspect-Object Flow) tree by applying coverage criteria such as condition coverage, polymorphic coverage, and loop coverage to woven sequence diagrams. In the AOF tree, each path from the root to a leaf is an abstract message sequence, indicating a template of test cases. A concrete test case is obtained by creating objects that satisfy the collective constraints in the template. Our empirical study shows that the model-based testing approach is capable of revealing several types of aspect-specific faults, including incorrect advice type, incorrect (weaker or stronger) pointcut strengths, and incorrect aspect precedence.

Aspects can be used in a harmful way that invalidates desired properties. Rigorous specification and analysis of aspect design is thus highly desirable. This paper presents an approach to model-checking state-based specification of aspect-oriented design. It is based on a rigorous formalism for capturing crosscutting concerns with respect to the design-level state models of classes. An aspect model not only encapsulates pointcuts and advice, but also supports inter-model declarations, aspect precedence, and references to the behaviors of other classes in advice models. For verification purposes, we convert the aspect-oriented state model of a system into woven models and further transform the woven models and the non-base class models into FSP processes. The generated FSP processes are checked by the LTSA model checker against the desired system properties. We have applied our approach to the modeling and verification of a non-trivial aspect-oriented cruise control system. A total of 21 properties that provide a comprehensive coverage of the system requirements are successfully formalized and verified.

This paper presents an aspect-oriented approach to integrated elicitation of functional and security requirements based on use case-driven development. We identify security threats with respect to use cases and adopt threat mitigations for preventing or reducing security threats. To capture crosscutting nature of threats and mitigations, we specify them as aspects that encapsulate pointcuts and advice. A threat (mitigation) pointcut is a collection of join points in use cases at which the use cases are threatened (secured); whereas threat/mitigation advice describes how a threat can become an attack (can be mitigated). Eliciting threats and mitigations as aspects provides a structured way for separating functional and security concerns

Design-level vulnerabilities are a major source of security risks in software. To improve trustworthiness of software design, this paper presents a formal threat-driven approach, which explores explicit behaviors of security threats as the mediator between security goals and applications of security features. Security threats are potential attacks, i.e., misuses and anomalies that violate the security goals of systems' intended functions. Security threats suggest what, where, and how security features for threat mitigation should be applied. To specify the intended functions, security threats, and threat mitigations of a security design as a whole, we exploit aspect-oriented Petri nets as a unified formalism. Intended functions and security threats are modeled by Petri nets, whereas threat mitigations are modeled by Petri net-based aspects due to the incremental and crosscutting nature of security features. The unified formalism facilitates verifying correctness of security threats against intended functions and verifying absence of security threats from integrated functions and threat mitigations. As a result, our approach can make software design provably secured from anticipated security threats and, thus, reduce significant design-level vulnerabilities. We demonstrate our approach through a systematic case study on the threat-driven modeling and verification of a real-world shopping cart application.

This paper presents a formal approach to threat-driven modeling and verification of secure software using aspect-oriented Petri nets. Based on the behavior model of intended functions, we identify and build formal models of security threats, which are potential misuses and anomalies of the intended functions that violate security goals. Threat mitigations are further modeled in an aspect-oriented paradigm. Taking Petri nets as a formal basis for modeling behaviors, threats, and mitigations as a whole, we verify properties of and consistency between behaviors and threats, and absence of identified threats from the integrated model of functions and threat mitigations. This makes it possible to achieve a design that is provably resistant to the anticipated threats and thus reduce significant design-level vulnerabilities.

An illumination invariant face recognition method based on neural network ensemble architecture is proposed. Given a face image with an arbitrary illumination direction, it can complete recognition in a uniform way with high performance without knowing or estimating the illumination direction. Experimental result shows that the recognition ratio of the ensemble architecture is higher than the conventional approach that uses a single neural network to recognize faces of a specific illumination direction.

This paper presents an approach to human-agent mixed teams for distributed team training, demonstrated through the integration of the domain independent multiagent architecture CAST with the military command-and-control simulation software DDD (distributed dynamic decision-making). We extend the CAST architecture in a way such that agents can replace any number of teammates on a DDD team. To capture the overall picture of teamwork, we explore the MALLET language in CAST for the specification of team structures and processes that involve both humans and agents.

How agents accomplish a goal task in a multi-agent system is usually specified by multi-agent plans built from basic actions (e.g. operators) of which the agents are capable. The plan specification provides the agents with a shared mental model for how they are supposed to collaborate with each other to achieve the common goal. Making sure that the plans are reliable and fit for the purpose for which they are designed is a critical problem with this approach. To address this problem, this paper presents a formal approach to modeling and analyzing multi-agent behaviors using Predicate/Transition (PrT) nets, a high- level formalism of Petri nets. We model a multi-agent problem by representing agent capabilities as transitions in PrT nets. To analyze a multi-agent PrT model, we adapt the planning graphs as a compact structure for reachability analysis, which is coherent to the concurrent semantics. We also demonstrate that one can analyze whether parallel actions specified in multi-agent plans can be executed in parallel and whether the plans can achieve the goal by analyzing the dependency relations among the transitions in the PrT model.

The process of agent migration is the major difference between logical code mobility of software agents and physical mobility of mobile nodes in ad hoc networks. Without considering agent transfer, it would make little sense to mention the modeling of strong code mobility, which aims to make a migrated agent restarted exactly from the state when it was stopped before migration. From the perspective of system's architecture, this paper proposes a two-layer approach for the formal modeling of logical agent mobility (LAM) using predicate/transition (PrT) nets. We view a mobile agent system as a set of agent spaces and agents could migrate from one space to another. Each agent space is explicitly abstracted to be a component, consisting of an environmental part and an internal connector dynamically binding agents with their environment. We use a system net, agent nets, and a connector net to model the environment, agents, and the connector, respectively. In particular, agent nets are packed up as parts of tokens in system nets, so that agent transfer and location change are naturally captured by transition firing (token game) in Petri nets. Agent nets themselves are active only at specific places and disabled at all the other places in a system net. The semantics of such a two-layer LAM model is defined by transforming it into a PrT net. This facilitates the analysis of several properties about location, state, and connection. In addition, this paper also presents a case study of modeling and analyzing an information retrieval system with mobile agents.

In a multi-agent system, how agents accomplish a goal task is usually specified by multi-agent plans built from basic actions (e.g. operators) of which the agents are capable. A critical problem with such an approach is how can the designer make sure the plans are reliable. To tackle this problem, this paper presents a formal approach for modeling and analyzing multi-agent behaviors using Predicate/Transition (PrT) nets, a high-level formalism of Petri nets. We construct a multi-agent model by representing agent capabilities as transitions. To verify a multi-agent PrT model, we adapt the planning graphs as a compact structure for the reachability analysis. We also demonstrate that, based on the PrT model, whether parallel actions specified in multi-agent plans can be executed in parallel and whether the plans guarantee the achievement of the goal can be verified by analyzing the dependency relations among the transitions.

The paper presents a Petri net based approach for architectural modeling of mobile agent systems. An agent template (net) is proposed to model a changing number of autonomous and communicative software agents. An agent space is explicitly abstracted as a component, consisting of mobility environment (system net), agent templates (agent nets), and internal connector (net). Agent transfer is naturally captured by transition firing. To assure the strong mobility, the agent's state is delivered during migration. Agent mobility in OMG's MASIF is also examined by formalizing the interoperable agent system architecture.

Agent oriented programming (AOP) is a special kind of object-oriented programming. It can be worked out best for open systems and has the potentials to become a very attractive technique in the future. In this paper, we describe a specification and programming language-SPLAW. The syntax and operational semantics of SPLAW are presented, and by means of labeled transition system, the proof theory is also provided. SPLAW is based on KQML, the standard inter-agent communication language, which makes it possible for agents written in SPLAW to interoperate with other agents obeying KQML.

This paper presents a knowledge based model description language KBMDL. It is taken as the basis of NUIDSS, an intelligent decision support system. Due to the flexible connection with a knowledge base, the language not only enhances the construction and the management of the model base, but also has the capability of both quantitative and qualitative analysis. The other features include graphic description and interface to model, data file and database. Based on KBMDL, semi-structured and non-structured problems are decomposed as various cooperative models where the relationships are contained in the domain knowledge base. This provides efficient support for decision making.>