Authscan: Automatic Extraction Of Web Authentication Protocols From Implementations,
2013
Singapore Management University
Authscan: Automatic Extraction Of Web Authentication Protocols From Implementations, Guangdong Bai, Jike Lei, Guozhu Meng, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Ideally, security protocol implementations should be formally verified before they are deployed. However, this is not true in practice. Numerous high-profile vulnerabilities have been found in web authentication protocol implementations, especially in single-sign on (SSO) protocols implementations recently. Much of the prior work on authentication protocol verification has focused on theoretical foundations and building scalable verification tools for checking manually-crafted specifications [17, 18, 44]. In this paper, we address a complementary problem of automatically extracting specifications from implementations. We propose AUTHSCAN, an end-to-end platform to automatically recover authentication protocol specifications from their implementations. AUTHSCAN finds a total of 7 security …
Verification Of Functional And Non-Functional Requirements Of Web Service Composition,
2013
Singapore Management University
Verification Of Functional And Non-Functional Requirements Of Web Service Composition, Manman Chen, Tian Huat Tan, Jun Sun, Yang Liu, Jun Pang, Xiaohong Li
Research Collection School Of Computing and Information Systems
Web services have emerged as an important technology nowadays. There are two kinds of requirements that are crucial to web service composition, which are functional and non-functional requirements. Functional requirements focus on functionality of the composed service, e.g., given a booking service, an example of functional requirements is that a flight ticket with price higher than $2000 will never be purchased. Non-functional requirements are concerned with the quality of service (QoS), e.g., an example of the booking service’s non-functional requirements is that the service will respond to the user within 5 seconds. Non-functional requirements are important to web service composition, …
Improving Model Checking Stateful Timed Csp With Non-Zenoness Through Clock-Symmetry Reduction,
2013
Singapore Management University
Improving Model Checking Stateful Timed Csp With Non-Zenoness Through Clock-Symmetry Reduction, Yuanjie Si, Jun Sun, Yang Liu, Ting Wang
Research Collection School Of Computing and Information Systems
Real-time system verification must deal with a special notion of ‘fairness’, i.e., clocks must always be able to progress. A system run which prevents clocks from progressing unboundedly is known as Zeno. Zeno runs are infeasible in reality and thus must be pruned during system verification. Though zone abstraction is an effective technique for model checking real-time systems, it is known that zone graphs (e.g., those generated from Timed Automata models) are too abstract to directly infer time progress and hence non-Zenoness. As a result, model checking with non-Zenoness (i.e., existence of a non-Zeno counterexample) based on zone graphs only …
A Utp Semantics For Communicating Processes With Shared Variables,
2013
Singapore Management University
A Utp Semantics For Communicating Processes With Shared Variables, Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong, Shengchao Qin
Research Collection School Of Computing and Information Systems
CSP# (Communicating Sequential Programs) is a modelling language designed for specifying concurrent systems by integrating CSP-like compositional operators with sequential programs updating shared variables. In this paper, we define an observation-oriented denotational semantics in an open environment for the CSP# language based on the UTP framework. To deal with shared variables, we lift traditional event-based traces into hybrid traces which consist of event-state pairs for recording process behaviours. We also define refinement to check process equivalence and present a set of algebraic laws which are established based on our denotational semantics. Our approach thus provides a rigorous means for reasoning …
Vtrust: A Formal Modeling And Verification Framework For Virtualization Systems,
2013
Singapore Management University
Vtrust: A Formal Modeling And Verification Framework For Virtualization Systems, Jianan Hao, Yang Liu, Wentong Cai, Guangdong Bai, Jun Sun
Research Collection School Of Computing and Information Systems
Virtualization is widely used for critical services like Cloud computing. It is desirable to formally verify virtualization systems. However, the complexity of the virtualization system makes the formal analysis a difficult task, e.g., sophisticated programs to manipulate low-level technologies, paged memory management, memory mapped I/O and trusted computing. In this paper, we propose a formal framework, vTRUST, to formally describe virtualization systems with a carefully designed abstraction. vTRUST includes a library to model configurable hardware components and technologies commonly used in virtualization. The system designer can thus verify virtualization systems on critical properties (e.g., confidentiality, verifiability, isolation and PCR consistency) …
Verifying Linearizability Via Optimized Refinement Checking,
2013
Singapore Management University
Verifying Linearizability Via Optimized Refinement Checking, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun, Shao Jie Zhang, Jin Song Dong Dong
Research Collection School Of Computing and Information Systems
Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: 1) All executions of concurrent operations are serializable, and 2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on …
Modeling And Verifying Hierarchical Real-Time Systems Using Stateful Timed Csp,
2013
Singapore Management University
Modeling And Verifying Hierarchical Real-Time Systems Using Stateful Timed Csp, Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André
Research Collection School Of Computing and Information Systems
Modeling and verifying complex real-time systems are challenging research problems. The de facto approach is based on Timed Automata, which are finite state automata equipped with clock variables. Timed Automata are deficient in modeling hierarchical complex systems. In this work, we propose a language called Stateful Timed CSP and an automated approach for verifying Stateful Timed CSP models. Stateful Timed CSP is based on Timed CSP and is capable of specifying hierarchical real-time systems. Through dynamic zone abstraction, finite-state zone graphs can be generated automatically from Stateful Timed CSP models, which are subject to model checking. Like Timed Automata, Stateful …
Raising The Game: Applying Theory And Analytics To Real-World Threats,
2013
Singapore Management University
Raising The Game: Applying Theory And Analytics To Real-World Threats, Singapore Management University
Perspectives@SMU
Safety and security are, on many levels, essential priorities for governments, businesses and individuals. While an increase of defence and security budgets may bring some assurance of peaceful times to come, it seems the world has no lack of insane perpetrators who can still somehow evade, breach, ambush, assail and attack as they please. Enter the “Bayesian Stackelberg Game”, a game theory model that can, and has been applied rather successfully to the allocation of security resources in the United States by Prof Milind Tambe, University of Southern California.
Special Issue On Medical Simulation,
2013
Old Dominion University
Special Issue On Medical Simulation, Michel Audette, Hanif M. Ladak
Computational Modeling & Simulation Engineering Faculty Publications
We would like to welcome you to this Special Issue on Medical Simulation, the first of its kind not only for SIMULATION: Transactions of The Society for Modeling and Simulation International, but for any technical journal. Our respective backgrounds are an indication of the technical and clinical breadth of medical simulation, as we approach the subject as primarily medical image analysis and biomechanics experts respectively, each with a variety of clinical interests spanning virtual reality (VR)–based neuro-, orthopedic and ear-nose-and-throat surgery. Moreover, we believe that the breadth of the papers that comprise this issue reflects an even broader perspective. After …
Impact Of Varied Low Resolution Phantoms On Intensity Modulated Proton Therapy Dose Distributions,
2013
California State University, San Bernardino
Impact Of Varied Low Resolution Phantoms On Intensity Modulated Proton Therapy Dose Distributions, Aarohi Shyam Padhye
Theses Digitization Project
The primary purpose of this thesis is to discuss the usefulness of image segmentation techniques in creating accurate proton dose distribution plans. The calculation of the proton dose distribution has to take into account the material (tissue, bone, brain) in the treatment area of the patients body.
Stereotactic Localization And Targeting Accuracy For Experimental Proton Radiosurgery,
2013
California State University, San Bernardino
Stereotactic Localization And Targeting Accuracy For Experimental Proton Radiosurgery, Yin Chen
Theses Digitization Project
The purpose of this study was to improve an existing experimental proton radiosurgery system at Loma Linda University Medical Center to reach sub-millimeter accuracy before proton radiosurgery with narrow beams can be used in a clinical trial. Protons, different from photons (i.e., x-rays or gamma rays), are charged with particles that slow down in matter and release a burst of energy near the end of their range (maximum depth of penetration), which is called the Bragg peak, named after the physicist William Henry Bragg who discovered it in 1903. Photon beams deliver most doses over a large area near the …
3d Face Animation With Opengl Es: An Android Application,
2013
California State University, San Bernardino
3d Face Animation With Opengl Es: An Android Application, Ihab Mohamad Zbib
Theses Digitization Project
Mobile applications have become ubiquitious with the increase in the popularity and computational power of mobile devices. They can now support rich multimedia user interactions. This project consists of the design and implementaiton of an Android application that renders and animates a three-dimensional model of a human head. The test is synthesized using an Android Text-to-Speech (TTS) engine. The application successfully implements a novel solution for the animated speech synchronization and opens the door for further work in the field of interactive animation. The project can be extended to become an interface for virtual remote communication or animated text messaging.
Fiducial-Free Alignment Verification Techniques For Intracranial Radiosurgery,
2013
California State University, San Bernardino
Fiducial-Free Alignment Verification Techniques For Intracranial Radiosurgery, Kenneth Matthew Williams
Theses Digitization Project
This thesis serves as the basis for a method using image registration to automate patient alignment in an effort to eliminate the dependency on the fiducial markers as well as improve the accuracy efficiency of the alignment process. Proton beams are an external beam modality of radiation therapy that can be used effectively for radiosurgical applications due to the dosimetry advantage of the Bragg peak. The Bragg peak is a phenomenon exploited by proton beam therapy to concentrate the effect of the beams on the tumor while minimizing damage to critical structures and other health tissues within the patient.
A New Phantom And Gradient Isocenter Estimation For Magnetic Resonance Imaging Distortion Correction,
2013
California State University, San Bernardino
A New Phantom And Gradient Isocenter Estimation For Magnetic Resonance Imaging Distortion Correction, Zongqi Cai
Theses Digitization Project
The purpose of this study was to develop and implement a numerical software based method that can accurately correct the distortion of MR images generated by 3T MRI scanner. To accomplish this, a new phantom has been designed from scratch to capture the distortions inside 3T MRI scanner. An algorithm has been developed, based on the unique geometric feature of the new phantom, to estimate the location of gradient isocenter of the magnetic field inside 3T MRI scanner for the first time.
Alternative Hull Detection Techniques For Preprocessing In Proton Computed Tomography Reconstruction,
2013
California State University, San Bernardino
Alternative Hull Detection Techniques For Preprocessing In Proton Computed Tomography Reconstruction, Blake Edward Schultze
Theses Digitization Project
The purpose of this study was to develop computationally efficient hull detection techniques appropriate for image reconstruction using sparse matrices. The hull detection techniques investigated were space carving (SC), modified space carving (MSC), and space modeling (SM) and these were compared to the cone-beam version of filtered back projection (FBP) algorithm in terms of their computation time and the quality of the object hull they produced.
Towards An Early Software Estimation Using Log-Linear Regression And A Multilayer Perceptron Model,
2013
University of Western Ontario
Towards An Early Software Estimation Using Log-Linear Regression And A Multilayer Perceptron Model, Ali Bou Nassif, Nfa-Estimation, Luiz Fernando Capretz
Electrical and Computer Engineering Publications
Software estimation is a tedious and daunting task in project management and software development. Software estimators are notorious in predicting software effort and they have been struggling in the past decades to provide new models to enhance software estimation. The most critical and crucial part of software estimation is when estimation is required in the early stages of the software life cycle where the problem to be solved has not yet been completely revealed. This paper presents a novel log-linear regression model based on the use case point model (UCP) to calculate the software effort based on use case diagrams. …
Eef-Cas: An Effort Estimation Framework With Customizable Attribute Selection,
2013
Western University
Eef-Cas: An Effort Estimation Framework With Customizable Attribute Selection, Katarina Grolinger, Besa Muslimi, Miriam A.M. Capretz, Mark Benko
Electrical and Computer Engineering Publications
Existing estimation frameworks generally provide one-size-fits-all solutions that fail to produce accurate estimates in most environments. Research has shown that the accomplishment of accurate effort estimates is a long-term process that, above all, requires the extensive collection of effort estimation data by each organization. Collected data is generally characterized by a set of attributes that are believed to affect the development effort. The attributes that most affect development effort vary widely depending on the type of product being developed and the environment in which it is being developed. Thus, any new estimation framework must offer the flexibility of customizable attribute …
Knowledge As A Service Framework For Disaster Data Management,
2013
Western University
Knowledge As A Service Framework For Disaster Data Management, Katarina Grolinger, Emna Mezghani, Miriam Am Capretz, Ernesto Exposito
Electrical and Computer Engineering Publications
Each year, a number of natural disasters strike across the globe, killing hundreds and causing billions of dollars in property and infrastructure damage. Minimizing the impact of disasters is imperative in today’s society. As the capabilities of software and hardware evolve, so does the role of information and communication technology in disaster mitigation, preparation, response, and recovery. A large quantity of disaster-related data is available, including response plans, records of previous incidents, simulation data, social media data, and Web sites. However, current data management solutions offer few or no integration capabilities. Moreover, recent advances in cloud computing, big data, and …
Extension Of Object-Oriented Metrics Suite For,
2013
Western University
Extension Of Object-Oriented Metrics Suite For, John Michura, Miriam A M Capretz, Shuying Wang
Electrical and Computer Engineering Publications
Software developers require information to understand the characteristics of systems, such as complexity and maintainability. In order to further understand and determine characteristics of object-oriented (OO) systems, this paper describes research that identifies attributes that are valuable in determining the difficulty in implementing changes during maintenance, as well as the possible effects that such changes may produce. A set of metrics are proposed to quantify and measure these attributes. The proposed complexity metrics are used to determine the difficulty in implementing changes through the measurement of method complexity, method diversity, and complexity density. The paper establishes impact metrics to determine …
A Hybrid Intelligent Model For Software Cost Estimation,
2013
Western University
A Hybrid Intelligent Model For Software Cost Estimation, Wei Lin Du, Luiz Fernando Capretz, Ali Bou Nassif, Danny Ho
Electrical and Computer Engineering Publications
Accurate software development effort estimation is critical to the success of software projects. Although many techniques and algorithmic models have been developed and implemented by practitioners, accurate software development effort prediction is still a challenging endeavor in the field of software engineering, especially in handling uncertain and imprecise inputs and collinear characteristics. In this paper, a hybrid intelligent model combining a neural network model integrated with fuzzy model (neuro-fuzzy model) has been used to improve the accuracy of estimating software cost. The performance of the proposed model is assessed by designing and conducting evaluation with published project and industrial data. …
