Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Engineering (458)
- Computer Engineering (300)
- Databases and Information Systems (266)
- Electrical and Computer Engineering (236)
- Social and Behavioral Sciences (217)
-
- Information Security (205)
- Software Engineering (170)
- Numerical Analysis and Scientific Computing (166)
- Mathematics (94)
- Life Sciences (87)
- Artificial Intelligence and Robotics (85)
- Programming Languages and Compilers (81)
- Communication (75)
- Graphics and Human Computer Interfaces (74)
- Theory and Algorithms (73)
- Law (71)
- Other Computer Sciences (71)
- OS and Networks (70)
- Computer Law (67)
- Legal Studies (65)
- Education (64)
- Forensic Science and Technology (64)
- Business (63)
- Physics (55)
- Statistics and Probability (55)
- Medicine and Health Sciences (46)
- Bioinformatics (40)
- Sociology (37)
- Institution
-
- Singapore Management University (361)
- TÜBİTAK (121)
- Missouri University of Science and Technology (111)
- University of Nebraska - Lincoln (73)
- Embry-Riddle Aeronautical University (71)
-
- Edith Cowan University (68)
- Purdue University (64)
- Brigham Young University (56)
- Wright State University (53)
- Old Dominion University (49)
- University of Texas at El Paso (46)
- California Polytechnic State University, San Luis Obispo (41)
- City University of New York (CUNY) (41)
- Marquette University (40)
- San Jose State University (40)
- Clemson University (35)
- Nova Southeastern University (32)
- Dartmouth College (24)
- University of Nebraska at Omaha (24)
- University for Business and Technology in Kosovo (22)
- University of Nevada, Las Vegas (21)
- Wayne State University (21)
- Utah State University (20)
- Southwestern Oklahoma State University (18)
- Portland State University (16)
- University of Texas at Arlington (16)
- Air Force Institute of Technology (15)
- Technological University Dublin (15)
- University of Central Florida (15)
- Minnesota State University, Mankato (13)
- Keyword
-
- Applied sciences (40)
- Security (31)
- Data mining (25)
- Machine learning (22)
- Big data (19)
-
- Digital forensics (19)
- Social media (18)
- Privacy (17)
- Algorithms (16)
- Classification (16)
- Education (16)
- Optimization (16)
- Android (15)
- Twitter (14)
- Authentication (12)
- Cloud computing (12)
- Computer science (12)
- Online learning (12)
- Visualization (12)
- Clustering (10)
- Image processing (10)
- Mobile (10)
- Technology (10)
- Wireless sensor networks (10)
- Genetic algorithm (9)
- [RSTDPub] (9)
- AHRC New York City (8)
- Community Engagement (8)
- Computer vision (8)
- Department of Computer Science and Engineering (8)
- Publication
-
- Research Collection School Of Computing and Information Systems (345)
- Turkish Journal of Electrical Engineering and Computer Sciences (121)
- Theses and Dissertations (52)
- Journal of Digital Forensics, Security and Law (50)
- The R Journal (47)
-
- Open Access Theses (37)
- Master's Projects (36)
- Computer Science Faculty Research & Creative Works (33)
- Departmental Technical Reports (CS) (33)
- Mathematics, Statistics and Computer Science Faculty Research and Publications (33)
- Journal of Undergraduate Research (32)
- Computer Science Faculty Publications (31)
- CCAC Theses and Dissertations (30)
- Research outputs 2014 to 2021 (25)
- Kno.e.sis Publications (24)
- Electrical and Computer Engineering Faculty Research & Creative Works (23)
- All Theses (22)
- Computer Science Technical Reports (22)
- Electronic Theses and Dissertations (22)
- Dissertations, Theses, and Capstone Projects (20)
- Master's Theses (20)
- Physics Faculty Research & Creative Works (20)
- UNLV Theses, Dissertations, Professional Papers, and Capstones (19)
- Oklahoma Research Day Abstracts (18)
- Annual ADFSL Conference on Digital Forensics, Security and Law (17)
- Doctoral Dissertations (17)
- Computer Science and Engineering Faculty Publications (16)
- Open Access Dissertations (16)
- All Graduate Theses and Dissertations, Spring 1920 to Summer 2023 (14)
- Australian Digital Forensics Conference (14)
- Publication Type
- File Type
Articles 811 - 840 of 1965
Full-Text Articles in Computer Sciences
Visualizing Instant Messaging Author Writeprints For Forensic Analysis, Angela Orebaugh, Jason Kinser, Jeremy Allnutt
Visualizing Instant Messaging Author Writeprints For Forensic Analysis, Angela Orebaugh, Jason Kinser, Jeremy Allnutt
Annual ADFSL Conference on Digital Forensics, Security and Law
As cybercrime continues to increase, new cyber forensics techniques are needed to combat the constant challenge of Internet anonymity. In instant messaging (IM) communications, criminals use virtual identities to hide their true identity, which hinders social accountability and facilitates cybercrime. Current instant messaging products are not addressing the anonymity and ease of impersonation over instant messaging. It is necessary to have IM cyber forensics techniques to assist in identifying cyber criminals as part of the criminal investigation. Instant messaging behavioral biometrics include online writing habits, which may be used to create an author writeprint to assist in identifying an author …
Botnet Forensic Investigation Techniques And Cost Evaluation, Brian Cusack
Botnet Forensic Investigation Techniques And Cost Evaluation, Brian Cusack
Annual ADFSL Conference on Digital Forensics, Security and Law
Botnets are responsible for a large percentage of damages and criminal activity on the Internet. They have shifted attacks from push activities to pull techniques for the distribution of malwares and continue to provide economic advantages to the exploiters at the expense of other legitimate Internet service users. In our research we asked; what is the cost of the procedural steps for forensically investigating a Botnet attack? The research method applies investigation guidelines provided by other researchers and evaluates these guidelines in terms of the cost to a digital forensic investigator. We conclude that investigation of Botnet attacks is both …
Development And Dissemination Of A New Multidisciplinary Undergraduate Curriculum In Digital Forensics, Masooda Bashir, Jenny A. Applequist, Roy H. Campbell, Lizanne Destefano, Gabriela L. Garcia, Anthony Lang
Development And Dissemination Of A New Multidisciplinary Undergraduate Curriculum In Digital Forensics, Masooda Bashir, Jenny A. Applequist, Roy H. Campbell, Lizanne Destefano, Gabriela L. Garcia, Anthony Lang
Annual ADFSL Conference on Digital Forensics, Security and Law
The Information Trust Institute (ITI) at the University of Illinois at Urbana-Champaign is developing an entirely new multidisciplinary undergraduate curriculum on the topic of digital forensics, and this paper presents the findings of the development process, including initial results and evaluation of a pilot offering of the coursework to students. The curriculum consists of a four-course sequence, including introductory and advanced lecture courses with parallel laboratory courses, followed by an advanced course. The content has been designed to reflect both the emerging national standards and the strong multidisciplinary character of the profession of digital forensics, and includes modules developed collaboratively …
Computer Forensics For Accountants, Grover S. Kearns
Computer Forensics For Accountants, Grover S. Kearns
Annual ADFSL Conference on Digital Forensics, Security and Law
Digital attacks on organizations are becoming more common and more sophisticated. Firms are interested in providing data security and having an effective means to respond to attacks. Accountants possess important investigative and analytical skills that serve to uncover fraud in forensic investigations. Some accounting students take courses in forensic accounting but few colleges offer a course in computer forensics for accountants. Educators wishing to develop such a course may find developing the curriculum daunting. A major element of such a course is the use of forensic software. This paper argues the importance of computer forensics to accounting students and offers …
Constant Rmr Transformation To Augment Reader-Writer Locks With Atomic Upgrade/Downgrade Support, Jake S. Leichtling
Constant Rmr Transformation To Augment Reader-Writer Locks With Atomic Upgrade/Downgrade Support, Jake S. Leichtling
Dartmouth College Undergraduate Theses
The reader-writer problem [1] seeks to provide a lock that protects some critical section of code for two classes of processes: readers and writers. Multiple readers can have access to the critical section simultaneously, but only one writer can have access to the critical section to the exclusion of all other processes. The difficulties in solving the reader-writer problem lie not only in developing a correct and efficient algorithm, but also in rigorously formulating the desirable properties for such an algorithm to have. Bhatt and Jayanti accomplished both of these tasks for several priority variants of the standard reader-writer problem …
Applying Memory Forensics To Rootkit Detection, Igor Korkin, Ivan Nesterov
Applying Memory Forensics To Rootkit Detection, Igor Korkin, Ivan Nesterov
Annual ADFSL Conference on Digital Forensics, Security and Law
Volatile memory dump and its analysis is an essential part of digital forensics. Among a number of various software and hardware approaches for memory dumping there are authors who point out that some of these approaches are not resilient to various anti-forensic techniques, and others that require a reboot or are highly platform dependent. New resilient tools have certain disadvantages such as low speed or vulnerability to rootkits which directly manipulate kernel structures, e.g., page tables. A new memory forensic system – Malware Analysis System for Hidden Knotty Anomalies (MASHKA) is described in this paper. It is resilient to popular …
The Federal Rules Of Civil Procedure: Politics In The 2013-2014 Revision, John W. Bagby, Byron Granda, Emily Benoit, Alexander Logan, Ryan Snell, Joseph J. Schwerha
The Federal Rules Of Civil Procedure: Politics In The 2013-2014 Revision, John W. Bagby, Byron Granda, Emily Benoit, Alexander Logan, Ryan Snell, Joseph J. Schwerha
Annual ADFSL Conference on Digital Forensics, Security and Law
Pre-trial discovery is perpetually controversial. Parties advantaged by strict privacy can often avoid justice when this is disadvantageous to their interests. Contrawise, parties advantaged by relaxed litigation privacy can achieve justice when all facts are accessible irrespective of their repositories, ownership or control. American-style pre-trial discovery in civil and regulatory enforcement is relatively rare around the world. U.S. discovery rules open nearly all relevant and non-privileged data for use by opposing parties. The traditional discovery process was costly and time consuming in the world of tangible paper data. However, these burdens have increased, rather than diminished as often predicted, as …
Testing And Evaluating The Harmonised Digital Forensic Investigation Process In Post Mortem Digital Investigation, Emilio R. Mumba, H. S. Venter
Testing And Evaluating The Harmonised Digital Forensic Investigation Process In Post Mortem Digital Investigation, Emilio R. Mumba, H. S. Venter
Annual ADFSL Conference on Digital Forensics, Security and Law
Existing digital forensic investigation process models have provided guidelines for identifying and preserving potential digital evidence captured from a crime scene. However, for any of the digital forensic investigation process models developed across the world to be adopted and fully applied by the scientific community, it has to be tested. For this reason, the Harmonized Digital Forensic Investigation Process (HDFIP) model, currently a working draft towards becoming an international standard for digital forensic investigations (ISO/IEC 27043), needs to be tested.
This paper, therefore, presents the findings of a case study used to test the HDFIP model implemented in the ISO/IEC …
Generation And Handling Of Hard Drive Duplicates As Piece Of Evidence, T. Kemmerich, F. Junge, N. Kuntze, C. Rudolph, B. Endicott-Popovsky, L. Großkopf
Generation And Handling Of Hard Drive Duplicates As Piece Of Evidence, T. Kemmerich, F. Junge, N. Kuntze, C. Rudolph, B. Endicott-Popovsky, L. Großkopf
Annual ADFSL Conference on Digital Forensics, Security and Law
An important area in digital forensics is images of hard disks. The correct production of the images as well as the integrity and authenticity of each hard disk image is essential for the probative force of the image to be used at court. Integrity and authenticity are under suspicion as digital evidence is stored and used by software based systems. Modifications to digital objects are hard or even impossible to track and can occur even accidentally. Even worse, vulnerabilities occur for all current computing systems. Therefore, it is difficult to guarantee a secure environment for forensic investigations. But intended deletions …
Internet Addiction To Child Pornography, Rachel Sitarz, Marcus Rogers, Lonnie Bentley, Eugene Jackson
Internet Addiction To Child Pornography, Rachel Sitarz, Marcus Rogers, Lonnie Bentley, Eugene Jackson
Annual ADFSL Conference on Digital Forensics, Security and Law
During the present age and time, it seems as though people in society have become addicted to nearly anything and everything, whether it be to a substance, an activity or an object. The Internet and pornography is no exception. While commonly thought of as a deviant behavior, many are displaying addictions towards the Internet and pornography. More alarming, however, are those who are viewing, downloading, or trading child pornography and displaying addictive Internet behaviors, for they are spending excessive amounts of time engaging in the proliferation of child pornographic materials. For this reason, addiction to the Internet and usage of …
Using Internet Artifacts To Profile A Child Pornography Suspect, Marcus K. Rogers, Kathryn C. Seigfried-Spellar
Using Internet Artifacts To Profile A Child Pornography Suspect, Marcus K. Rogers, Kathryn C. Seigfried-Spellar
Annual ADFSL Conference on Digital Forensics, Security and Law
Digital evidence plays a crucial role in child pornography investigations. However, in the following case study, the authors argue that the behavioral analysis or “profiling” of digital evidence can also play a vital role in child pornography investigations. The following case study assessed the Internet Browsing History (Internet Explorer Bookmarks, Mozilla Bookmarks, and Mozilla History) from a suspected child pornography user’s computer. The suspect in this case claimed to be conducting an ad hoc law enforcement investigation. After the URLs were classified (Neutral; Adult Porn; Child Porn; Adult Dating sites; Pictures from Social Networking Profiles; Chat Sessions; Bestiality; Data Cleaning; …
Life (Logical Iosforensics Examiner): An Open Source Iosbackup Forensics Examination Tool, Ibrahim Baggili, Shadi Al Awawdeh, Jason Moore
Life (Logical Iosforensics Examiner): An Open Source Iosbackup Forensics Examination Tool, Ibrahim Baggili, Shadi Al Awawdeh, Jason Moore
Annual ADFSL Conference on Digital Forensics, Security and Law
In this paper, we present LiFE (Logical iOS Forensics Examiner), an open source iOS backup forensics examination tool. This tool helps both researchers and practitioners alike in both understanding the backup structures of iOS devices and forensically examining iOS backups. The tool is currently capable of parsing device information, call history, voice messages, GPS locations, conversations, notes, images, address books, calendar entries, SMS messages, Aux locations, facebook data and e-mails. The tool consists of both a manual interface (where the user is able to manually examine the backup structures) and an automated examination interface (where the tool pulls out evidence …
Why Penetration Testing Is A Limited Use Choice For Sound Cyber Security Practice, Craig Valli, Andrew Woodward, Peter Hannay, Mike Johnstone
Why Penetration Testing Is A Limited Use Choice For Sound Cyber Security Practice, Craig Valli, Andrew Woodward, Peter Hannay, Mike Johnstone
Annual ADFSL Conference on Digital Forensics, Security and Law
Penetration testing of networks is a process that is overused when demonstrating or evaluating the cyber security posture of an organisation. Most penetration testing is not aligned with the actual intent of the testing, but rather is driven by a management directive of wanting to be seen to be addressing the issue of cyber security. The use of penetration testing is commonly a reaction to an adverse audit outcome or as a result of being penetrated in the first place. Penetration testing used in this fashion delivers little or no value to the organisation being tested for a number of …
Awareness Of Scam E-Mails: An Exploratory Research Study, Tejashree D. Datar, Kelly A. Cole, Marcus K. Rogers
Awareness Of Scam E-Mails: An Exploratory Research Study, Tejashree D. Datar, Kelly A. Cole, Marcus K. Rogers
Annual ADFSL Conference on Digital Forensics, Security and Law
The goal of this research was to find the factors that influence a user’s ability to identify e-mail scams. It also aimed to understand user’s awareness regarding e-mail scams and actions that need to be taken if and when victimized. This study was conducted on a university campus with 163 participants. This study presented the participants with two scam e-mails and two legitimate e-mails and asked the participants to correctly identify these e-mails as scam or legitimate. The study focused on the ability of people to differentiate between scam and legitimate e-mails. The study attempted to determine factors that influence …
Chain Match: An Algorithm For Finding A Perfect Matching Of A Regular Bipartite Multigraph, Stefanie L. Ostrowski
Chain Match: An Algorithm For Finding A Perfect Matching Of A Regular Bipartite Multigraph, Stefanie L. Ostrowski
Dartmouth College Undergraduate Theses
We consider the problem of performing an edge coloring of a d-regular bipartite multigraph G = (V, E). While an edge coloring can be found by repeatedly performing Euler partitions on G, doing so requires that the degree of G be a power of 2. One way to allow the Euler partitioning method to continue in cases where d is not a power of 2 is to remove a perfect matching from the graph after any partition that results in a graph with an odd degree. If this perfect matching can be identified in O(E) time, we can maintain the …
Detection Of Land Use Change In Lake Maumelle Watershed Critical Management Area: Image Processing And Gis Integration Approach, Ling Zhang
Theses and Dissertations
Land use in the Lake Maumelle watershed is expected to undergo significant changes in the next several decades, with residential developments replacing forest in many areas. These land use changes have the potential to increase pollutant loads and degrade water quality in the lake. Detecting the land use and land cover changes is therefore a critical requirement for effective land management. Therefore, the research on the cost-effective methodology of detection of land use change is critical and of extreme significance. The first objective of this study is to develop an effective image classification method using very high resolution remote sensing …
Qr Codes For The Dead, Tamara Kneese
Qr Codes For The Dead, Tamara Kneese
Media Studies
Graveyards are becoming smart spaces, but will today's technology last for eternity?
Twill: A Hybrid Microcontroller-Fpga Framework For Parallelizing Single-Threaded C Programs, Douglas S. Gallatin, Aaron Keen, Chris Lupo, John Y. Oliver
Twill: A Hybrid Microcontroller-Fpga Framework For Parallelizing Single-Threaded C Programs, Douglas S. Gallatin, Aaron Keen, Chris Lupo, John Y. Oliver
Computer Science and Software Engineering
Increasingly System-On-A-Chip platforms which incorporate both microprocessors and re-programmable logic are being utilized across several fields ranging from the automotive industry to network infrastructure. Unfortunately, the development tools accompanying these products leave much to be desired, requiring knowledge of both traditional embedded systems languages like C and hardware description languages like Verilog. We propose to bridge this gap with Twill, a truly automatic hybrid compiler that can take advantage of the parallelism inherent in these platforms. Twill can extract long-running threads from single threaded C code and distribute these threads across the hardware and software domains to more fully utilize …
A Systematic Security Evaluation Of Android’S Multi-User Framework, Edward Paul Ratazzi, Yousra Aafer, Amit Ahlawat, Hao Hao, Yifei Wang, Wenliang Du
A Systematic Security Evaluation Of Android’S Multi-User Framework, Edward Paul Ratazzi, Yousra Aafer, Amit Ahlawat, Hao Hao, Yifei Wang, Wenliang Du
Electrical Engineering and Computer Science - All Scholarship
Like many desktop operating systems in the 1990s, Android is now in the process of including support for multiuser scenarios. Because these scenarios introduce new threats to the system, we should have an understanding of how well the system design addresses them. Since the security implications of multi-user support are truly pervasive, we developed a systematic approach to studying the system and identifying problems. Unlike other approaches that focus on specific attacks or threat models, ours systematically identifies critical places where access controls are not present or do not properly identify the subject and object of a decision. Finding these …
Hydrographic Surface Modeling Through A Raster Based Spline Creation Method, Julie G. Alexander
Hydrographic Surface Modeling Through A Raster Based Spline Creation Method, Julie G. Alexander
LSU New Orleans Theses and Dissertations
The United States Army Corp of Engineers relies on accurate and detailed surface models for various construction projects and preventative measures. To aid in these efforts, it is necessary to work for advancements in surface model creation. Current methods for model creation include Delaunay triangulation, raster grid interpolation, and Hydraulic Spline grid generation. While these methods produce adequate surface models, attempts for improved methods can still be made.
A method for raster based spline creation is presented as a variation of the Hydraulic Spline algorithm. By implementing Hydraulic Splines in raster data instead of vector data, the model creation process …
Applying The Poincaré Recurrence Theorem To Billiards, Aaron Smith
Applying The Poincaré Recurrence Theorem To Billiards, Aaron Smith
Honors Theses
The Poincaré recurrence theorem is one of the first and most fundamental theorems of ergodic theory. When applied to a dynamical system satisfying the theorem's hypothesis, it roughly states that the system will, within a finite amount of time, return to a state arbitrarily close to its initial state. This result is intriguing and controversial, providing a contradiction with the Second Law of Thermodynamics known as the recurrence paradox. Here, we treat a set of pool balls on a billiard table as a dynamical system that satisfies the hypotheses of the Poincaré recurrence theorem. We prove that time is a …
Global Edf Scheduling For Parallel Real-Time Tasks, Jing Li
Global Edf Scheduling For Parallel Real-Time Tasks, Jing Li
McKelvey School of Engineering Graduate Student Theses & Dissertations
As multicore processors become ever more prevalent, it is important for real-time programs to take advantage of intra-task parallelism in order to support computation-intensive applications with tight deadlines. In this thesis, we consider the Global Earliest Deadline First (GEDF) scheduling policy for task sets consisting of parallel tasks. Each task can be represented by a directed acyclic graph (DAG) where nodes represent computational work and edges represent dependences between nodes. In this model, we prove that GEDF provides a capacity augmentation bound of 4-2/m and a resource augmentation bound of 2-1/m. The capacity augmentation bound acts as a linear-time schedulability …
Digital Circuit Projects: An Overview Of Digital Circuits Through Implementing Integrated Circuits - Second Edition, Charles W. Kann
Digital Circuit Projects: An Overview Of Digital Circuits Through Implementing Integrated Circuits - Second Edition, Charles W. Kann
Open Educational Resources
Digital circuits, often called Integrated Circuits or ICs, are the central building blocks of a Central Processing Unit (CPU). To understand how a computer works, it is essential to understand the digital circuits which make up the CPU. This text introduces the most important of these digital circuits; adders, decoders, multiplexers, D flip-flops, and simple state machines.
What makes this textbook unique is that it puts the ability to understand these circuits into the hands of anyone, from hobbyists to students studying Computer Science. This text is designed to teach digital circuits using simple projects the reader can implement. But …
Generalized Mandelbrot Sets, Aaron Schlenker
Generalized Mandelbrot Sets, Aaron Schlenker
Undergraduate Honors Thesis Collection
A complex point Z0 is defined to be a member of the famous Mandelbrot set fractal when the iterative process using the function Z2 stays bounded when applied to Z0. We investigate what happens if we change the iterative process so that Z2 is now composed with, for example, a Mobius transformation, indexed on a parameter a. The Mandelbrot set corresponds to a = O. What happens when we change a = 0 to other values, repeating the iterative process and then drawing the sets? Do these Generalized Mandelbrot sets have similar properties to …
Decaf: A New Event Detection Logic For The Purpose Of Fusing Delineated-Continuous Spatial Information, Kerry Q. Hart
Decaf: A New Event Detection Logic For The Purpose Of Fusing Delineated-Continuous Spatial Information, Kerry Q. Hart
School of Computing: Dissertations, Theses, and Student Research
Geospatial information fusion is the process of synthesizing information from complementary data sources located at different points in space and time. Spatial phenomena are often measured at discrete locations by sensor networks, technicians, and volunteers; yet decisions often require information about locations where direct measurements do not exist. Traditional methods assume the spatial phenomena to be either discrete or continuous, an assumption that underlies and informs all subsequent analysis. Yet certain phenomena defy this dichotomy, alternating as they move across spatial and temporal scales. Precipitation, for example, appears continuous at large scales, but it can be temporally decomposed into discrete …
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP …
Gpu Accelerated Counterexample Generation In Ltl Model Checking, Zhimin Wu, Yang Liu, Yun Liang, Jun Sun
Gpu Accelerated Counterexample Generation In Ltl Model Checking, Zhimin Wu, Yang Liu, Yun Liang, Jun Sun
Research Collection School Of Computing and Information Systems
Strongly Connected Component (SCC) based searching is one of the most popular LTL model checking algorithms. When the SCCs are huge, the counterexample generation process can be time-consuming, especially when dealing with fairness assumptions. In this work, we propose a GPU accelerated counterexample generation algorithm, which improves the performance by parallelizing the Breadth First Search (BFS) used in the counterexample generation. BFS work is irregular, which means it is hard to allocate resources and may suffer from imbalanced load. We make use of the features of latest CUDA Compute Architecture-NVIDIA Kepler GK110 to achieve the dynamic parallelism and memory hierarchy …
Practical Analysis Framework For Software-Based Attestation Scheme, Li Li, Hong Hu, Jun Sun, Yang Liu, Dong Jin Song
Practical Analysis Framework For Software-Based Attestation Scheme, Li Li, Hong Hu, Jun Sun, Yang Liu, Dong Jin Song
Research Collection School Of Computing and Information Systems
An increasing number of ”smart” embedded devices are employed in our living environment nowadays. Unlike traditional computer systems, these devices are often physically accessible to the attackers. It is therefore almost impossible to guarantee that they are un-compromised, i.e., that indeed the devices are executing the intended software. In such a context, software-based attestation is deemed as a promising solution to validate their software integrity. It guarantees that the software running on the embedded devices are un-compromised without any hardware support. However, designing software-based attestation protocols are shown to be error-prone. In this work, we develop a framework for design …
A Hybrid Model Of Connectors In Cyber-Physical Systems, Xiaohong Chen, Jun Sun, Meng Sun Sun
A Hybrid Model Of Connectors In Cyber-Physical Systems, Xiaohong Chen, Jun Sun, Meng Sun Sun
Research Collection School Of Computing and Information Systems
Compositional coordination models and languages play an important role in cyber-physical systems (CPSs). In this paper, we introduce a formal model for describing hybrid behaviors of connectors in CPSs. We extend the constraint automata model, which is used as the semantic model for the exogenous channel-based coordination language Reo, to capture the dynamic behavior of connectors in CPSs where the discrete and continuous dynamics co-exist and interact with each other. In addition to the formalism, we also provide a theoretical compositional approach for constructing the product automata for a Reo circuit, which is typically obtained by composing several primitive connectors …
Tauth: Verifying Timed Security Protocols, Li Li, Jun Sun, Yang Liu, Jin Song Dong
Tauth: Verifying Timed Security Protocols, Li Li, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Quantitative timing is often relevant to the security of systems, like web applications, cyber-physical systems, etc. Verifying timed security protocols is however challenging as both arbitrary attacking behaviors and quantitative timing may lead to undecidability. In this work, we develop a service framework to support intuitive modeling of the timed protocol, as well as automatic verification with an unbounded number of sessions. The partial soundness and completeness of our verification algorithms are formally defined and proved. We implement our method into a tool called TAuth and the experiment results show that our approach is efficient and effective in both finding …