Biblio

Found 7524 results

Filters: Keyword is Metrics  [Clear All Filters]
2017-03-27
Phull, Sona, Som, Subhranil.  2016.  Symmetric Cryptography Using Multiple Access Circular Queues (MACQ). Proceedings of the Second International Conference on Information and Communication Technology for Competitive Strategies. :107:1–107:6.

In order to provide secure data communication in present cyber space world, a stronger encryption technique becomes a necessity that can help people to protect their sensitive information from cryptanalyst. This paper proposes a novel symmetric block cipher algorithm that uses multiple access circular queues (MACQs) of variable lengths for diffusion of information to a greater extent. The keys are randomly generated and will be of variable lengths depending upon the size of each MACQ.A number of iterations of circular rotations, swapping of elements and XORing the key with queue elements are performed on each MACQ. S-box is used so that the relationship between the key and the cipher text remains indeterminate or obscure. These operations together will help in transforming the cipher into a much more complex and secure block cipher. This paper attempt to propose an encryption algorithm that is secure and fast.

2017-05-22
Pawar, Shwetambari, Jain, Nilakshi, Deshpande, Swati.  2016.  System Attribute Measures of Network Security Analyzer. Proceedings of the ACM Symposium on Women in Research 2016. :51–54.

In this paper, we have mentioned a method to find the performance of projectwhich detects various web - attacks. The project is capable to identifying and preventing attacks like SQL Injection, Cross – Site Scripting, URL rewriting, Web server 400 error code etc. The performance of system is detected using the system attributes that are mentioned in this paper. This is also used to determine efficiency of the system.

2017-11-27
Checkoway, Stephen, Maskiewicz, Jacob, Garman, Christina, Fried, Joshua, Cohney, Shaanan, Green, Matthew, Heninger, Nadia, Weinmann, Ralf-Philipp, Rescorla, Eric, Shacham, Hovav.  2016.  A Systematic Analysis of the Juniper Dual EC Incident. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. :468–479.

In December 2015, Juniper Networks announced multiple security vulnerabilities stemming from unauthorized code in ScreenOS, the operating system for their NetScreen VPN routers. The more sophisticated of these vulnerabilities was a passive VPN decryption capability, enabled by a change to one of the elliptic curve points used by the Dual EC pseudorandom number generator. In this paper, we describe the results of a full independent analysis of the ScreenOS randomness and VPN key establishment protocol subsystems, which we carried out in response to this incident. While Dual EC is known to be insecure against an attacker who can choose the elliptic curve parameters, Juniper had claimed in 2013 that ScreenOS included countermeasures against this type of attack. We find that, contrary to Juniper's public statements, the ScreenOS VPN implementation has been vulnerable since 2008 to passive exploitation by an attacker who selects the Dual EC curve point. This vulnerability arises due to apparent flaws in Juniper's countermeasures as well as a cluster of changes that were all introduced concurrently with the inclusion of Dual EC in a single 2008 release. We demonstrate the vulnerability on a real NetScreen device by modifying the firmware to install our own parameters, and we show that it is possible to passively decrypt an individual VPN session in isolation without observing any other network traffic. We investigate the possibility of passively fingerprinting ScreenOS implementations in the wild. This incident is an important example of how guidelines for random number generation, engineering, and validation can fail in practice.

2017-10-13
Saeed, Ahmed, Ahmadinia, Ali, Just, Mike.  2016.  Tag-Protector: An Effective and Dynamic Detection of Out-of-bound Memory Accesses. Proceedings of the Third Workshop on Cryptography and Security in Computing Systems. :31–36.

Programming languages permitting immediate memory accesses through pointers often result in applications having memory-related errors, which may lead to unpredictable failures and security vulnerabilities. A light-weight solution is presented in this paper to tackle such illegal memory accesses dynamically in C/C++ based applications. We propose a new and effective method of instrumenting an application's source code at compile time in order to detect out-of-bound memory accesses. It is based on creating tags, to be coupled with each memory allocation and then placing additional tag checking instructions for each access made to the memory. The proposed solution is evaluated by instrumenting applications from the BugBench benchmark suite and publicly available benchmark software, Runtime Intrusion Prevention Evaluator (RIPE), detecting all the bugs successfully. The performance and memory overhead is further analysed by instrumenting and executing real world applications.

2017-09-05
Luh, Robert, Schrittwieser, Sebastian, Marschalek, Stefan.  2016.  TAON: An Ontology-based Approach to Mitigating Targeted Attacks. Proceedings of the 18th International Conference on Information Integration and Web-based Applications and Services. :303–312.

Targeted attacks on IT systems are a rising threat against the confidentiality of sensitive data and the availability of systems and infrastructures. Planning for the eventuality of a data breach or sabotage attack has become an increasingly difficult task with the emergence of advanced persistent threats (APTs), a class of highly sophisticated cyber-attacks that are nigh impossible to detect using conventional signature-based systems. Understanding, interpreting, and correlating the particulars of such advanced targeted attacks is a major research challenge that needs to be tackled before behavior-based approaches can evolve from their current state to truly semantics-aware solutions. Ontologies offer a versatile foundation well suited for depicting the complex connections between such behavioral data and the diverse technical and organizational properties of an IT system. In order to facilitate the development of novel behavior-based detection systems, we present TAON, an OWL-based ontology offering a holistic view on actors, assets, and threat details, which are mapped to individual abstracted events and anomalies that can be detected by today's monitoring data providers. TOAN offers a straightforward means to plan an organization's defense against APTs and helps to understand how, why, and by whom certain resources are targeted. Populated by concrete data, the proposed ontology becomes a smart correlation framework able to combine several data sources into a semantic assessment of any targeted attack.

2017-05-22
de Chérisey, Eloi, Guilley, Sylvain, Rioul, Olivier, Jayasinghe, Darshana.  2016.  Template Attacks with Partial Profiles and Dirichlet Priors: Application to Timing Attacks. Proceedings of the Hardware and Architectural Support for Security and Privacy 2016. :7:1–7:8.

In order to retrieve the secret key in a side-channel attack, the attacker computes distinguisher values using all the available data. A profiling stage is very useful to provide some a priori information about the leakage model. However, profiling is essentially empirical and may not be exhaustive. Therefore, during the attack, the attacker may come up on previously unseen data, which can be troublesome. A lazy workaround is to ignore all such novel observations altogether. In this paper, we show that this is not optimal and can be avoided. Our proposed techniques eventually improve the performance of classical information-theoretic distinguishers in terms of success rate.

2017-03-27
Batselier, Kim, Chen, Zhongming, Liu, Haotian, Wong, Ngai.  2016.  A Tensor-based Volterra Series Black-box Nonlinear System Identification and Simulation Framework. Proceedings of the 35th International Conference on Computer-Aided Design. :17:1–17:7.

Tensors are a multi-linear generalization of matrices to their d-way counterparts, and are receiving intense interest recently due to their natural representation of high-dimensional data and the availability of fast tensor decomposition algorithms. Given the input-output data of a nonlinear system/circuit, this paper presents a nonlinear model identification and simulation framework built on top of Volterra series and its seamless integration with tensor arithmetic. By exploiting partially-symmetric polyadic decompositions of sparse Toeplitz tensors, the proposed framework permits a pleasantly scalable way to incorporate high-order Volterra kernels. Such an approach largely eludes the curse of dimensionality and allows computationally fast modeling and simulation beyond weakly nonlinear systems. The black-box nature of the model also hides structural information of the system/circuit and encapsulates it in terms of compact tensors. Numerical examples are given to verify the efficacy, efficiency and generality of this tensor-based modeling and simulation framework.

2017-09-19
Xie, Tao, Enck, William.  2016.  Text Analytics for Security: Tutorial. Proceedings of the Symposium and Bootcamp on the Science of Security. :124–125.

Computing systems that make security decisions often fail to take into account human expectations. This failure occurs because human expectations are typically drawn from in textual sources (e.g., mobile application description and requirements documents) and are hard to extract and codify. Recently, researchers in security and software engineering have begun using text analytics to create initial models of human expectation. In this tutorial, we provide an introduction to popular techniques and tools of natural language processing (NLP) and text mining, and share our experiences in applying text analytics to security problems. We also highlight the current challenges of applying these techniques and tools for addressing security problems. We conclude the tutorial with discussion of future research directions.

2017-05-19
Carter, Lemuria, McBride, Maranda.  2016.  Texting While Driving Among Teens: Exploring User Perceptions to Identify Policy Recommendations. Proceedings of the 17th International Digital Government Research Conference on Digital Government Research. :375–378.

Texting while driving has emerged as a significant threat to citizen safety. In this study, we utilize general deterrence theory (GDT), protection motivation theory and personality traits to evaluate texting while driving (TWD) compliance intentions among teenage drivers. This paper presents the results of our pilot study. We administered an online survey to 105 teenage and young adult drivers. The potential implications for research and practice and policy are discussed.

2017-09-05
Huang, Haixing, Song, Jinghe, Lin, Xuelian, Ma, Shuai, Huai, Jinpeng.  2016.  TGraph: A Temporal Graph Data Management System. Proceedings of the 25th ACM International on Conference on Information and Knowledge Management. :2469–2472.

Temporal graphs are a class of graphs whose nodes and edges, together with the associated properties, continuously change over time. Recently, systems have been developed to support snapshot queries over temporal graphs. However, these systems barely support aggregate time range queries. Moreover, these systems cannot guarantee ACID transactions, an important feature for data management systems as long as concurrent processing is involved. To solve these issues, we design and develop TGraph, a temporal graph data management system, that assures the ACID transaction feature, and supports fast temporal graph queries.

2017-05-16
Shrivastava, Anshumali, Konig, Arnd Christian, Bilenko, Mikhail.  2016.  Time Adaptive Sketches (Ada-Sketches) for Summarizing Data Streams. Proceedings of the 2016 International Conference on Management of Data. :1417–1432.

Obtaining frequency information of data streams, in limited space, is a well-recognized problem in literature. A number of recent practical applications (such as those in computational advertising) require temporally-aware solutions: obtaining historical count statistics for both time-points as well as time-ranges. In these scenarios, accuracy of estimates is typically more important for recent instances than for older ones; we call this desirable property Time Adaptiveness. With this observation, [20] introduced the Hokusai technique based on count-min sketches for estimating the frequency of any given item at any given time. The proposed approach is problematic in practice, as its memory requirements grow linearly with time, and it produces discontinuities in the estimation accuracy. In this work, we describe a new method, Time-adaptive Sketches, (Ada-sketch), that overcomes these limitations, while extending and providing a strict generalization of several popular sketching algorithms. The core idea of our method is inspired by the well-known digital Dolby noise reduction procedure that dates back to the 1960s. The theoretical analysis presented could be of independent interest in itself, as it provides clear results for the time-adaptive nature of the errors. An experimental evaluation on real streaming datasets demonstrates the superiority of the described method over Hokusai in estimating point and range queries over time. The method is simple to implement and offers a variety of design choices for future extensions. The simplicity of the procedure and the method's generalization of classic sketching techniques give hope for wide applicability of Ada-sketches in practice.

2017-05-17
Shrivastava, Aviral, Derler, Patricia, Baboud, Ya-Shian Li, Stanton, Kevin, Khayatian, Mohammad, Andrade, Hugo A., Weiss, Marc, Eidson, John, Chandhoke, Sundeep.  2016.  Time in Cyber-physical Systems. Proceedings of the Eleventh IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis. :4:1–4:10.

Many modern cyber-physical systems (CPS), especially industrial automation systems, require the actions of multiple computational systems to be performed at much higher rates and more tightly synchronized than is possible with ad hoc designs. Time is the common entity that computing and physical systems in CPS share, and correct interfacing of that is essential to flawless functionality of a CPS. Fundamental research is needed on ways to synchronize clocks of computing systems to a high degree, and on design methods that enable building blocks of CPS to perform actions at specified times. To realize the potential of CPS in the coming decades, suitable ways to specify distributed CPS applications are needed, including their timing requirements, ways to specify the timing of the CPS components (e.g. sensors, actuators, computing platform), timing analysis to determine if the application design is possible using the components, confident top-down design methodologies that can ensure that the system meets its timing requirements, and ways and methodologies to test and verify that the system meets the timing requirements. Furthermore, strategies for securing timing need to be carefully considered at every CPS design stage and not simply added on. This paper exposes these challenges of CPS development, points out limitations of previous approaches, and provides some research directions towards solving these challenges.

2017-09-26
Zhang, Zhengkui, Nielsen, Brian, Larsen, Kim G..  2016.  Time Optimal Reachability Analysis Using Swarm Verification. Proceedings of the 31st Annual ACM Symposium on Applied Computing. :1634–1640.

Time optimal reachability analysis employs model-checking to compute goal states that can be reached from an initial state with a minimal accumulated time duration. The model-checker may produce a corresponding diagnostic trace which can be interpreted as a feasible schedule for many scheduling and planning problems, response time optimization etc. We propose swarm verification to accelerate time optimal reachability using the real-time model-checker Uppaal. In swarm verification, a large number of model checker instances execute in parallel on a computer cluster using different, typically randomized search strategies. We develop four swarm algorithms and evaluate them with four models in terms scalability, and time- and memory consumption. Three of these cooperate by exchanging costs of intermediate solutions to prune the search using a branch-and-bound approach. Our results show that swarm algorithms work much faster than sequential algorithms, and especially two using combinations of random-depth-first and breadth-first show very promising performance.

2017-08-22
Jarrah, Hazim, Chong, Peter, Sarkar, Nurul I., Gutierrez, Jairo.  2016.  A Time-Free Comparison-Based System-Level Fault Diagnostic Model for Highly Dynamic Networks. Proceedings of the 11th International Conference on Queueing Theory and Network Applications. :12:1–12:6.

This paper considers the problem of system-level fault diagnosis in highly dynamic networks. The existing fault diagnostic models deal mainly with static faults and have limited capabilities to handle dynamic networks. These fault diagnostic models are based on timers that work on a simple timeout mechanism to identify the node status, and often make simplistic assumptions for system implementations. To overcome the above problems, we propose a time-free comparison-based diagnostic model. Unlike the traditional models, the proposed model does not rely on timers and is more suitable for use in dynamic network environments. We also develop a novel comparison-based fault diagnosis protocol for identifying and diagnosing dynamic faults. The performance of the protocol has been analyzed and its correctness has been proved.

2017-09-26
Walfield, Neal H., Koch, Werner.  2016.  TOFU for OpenPGP. Proceedings of the 9th European Workshop on System Security. :2:1–2:6.

We present the design and implementation of a trust-on-first-use (TOFU) policy for OpenPGP. When an OpenPGP user verifies a signature, TOFU checks that the signer used the same key as in the past. If not, this is a strong indicator that a key is a forgery and either the message is also a forgery or an active man-in-the-middle attack (MitM) is or was underway. That is, TOFU can proactively detect new attacks if the user had previously verified a message from the signer. And, it can reactively detect an attack if the signer gets a message through. TOFU cannot, however, protect against sustained MitM attacks. Despite this weakness, TOFU's practical security is stronger than the Web of Trust (WoT), OpenPGP's current trust policy, for most users. The problem with the WoT is that it requires too much user support. TOFU is also better than the most popular alternative, an X.509-based PKI, which relies on central servers whose certification processes are often sloppy. In this paper, we outline how TOFU can be integrated into OpenPGP; we address a number of potential attacks against TOFU; and, we show how TOFU can work alongside the WoT. Our implementation demonstrates the practicality of the approach.

2017-05-16
Bandyopadhyay, Bortik, Fuhry, David, Chakrabarti, Aniket, Parthasarathy, Srinivasan.  2016.  Topological Graph Sketching for Incremental and Scalable Analytics. Proceedings of the 25th ACM International on Conference on Information and Knowledge Management. :1231–1240.

We propose a novel, scalable, and principled graph sketching technique based on minwise hashing of local neighborhood. For an n-node graph with e-edges (e textgreatertextgreater n), we incrementally maintain in real-time a minwise neighbor sampled subgraph using k hash functions in O(n x k) memory, limit being user-configurable by the parameter k. Symmetrization and similarity based techniques can recover from these data structures a significant portion of the original graph. We present theoretical analysis of the minwise sampling strategy and also derive unbiased estimators for important graph properties such as triangle count and neighborhood overlap. We perform an extensive empirical evaluation of our graph sketch and it's derivatives on a wide variety of real-world graph data sets drawn from different application domains using important large network analysis algorithms: local and global clustering coefficient, PageRank, and local graph sparsification. With bounded memory, the quality of results using the sketch representation is competitive against baselines which use the full graph, and the computational performance is often better. Our framework is flexible and configurable to be leveraged by numerous other graph analytics algorithms, potentially reducing the information mining time on large streamed graphs for a variety of applications.

2017-09-05
Ghanim, Yasser.  2016.  Toward a Specialized Quality Management Maturity Assessment Model. Proceedings of the 2Nd Africa and Middle East Conference on Software Engineering. :1–8.

SW Quality Assessment models are either too broad such as CMMI-DEV and SPICE that cover the full software development life cycle (SDLC), or too narrow such as TMMI and TPI that focus on testing. Quality Management as a main concern within the software industry is broader than the concept of testing. The V-Model sets a broader view with the concepts of Verification and Validation. Quality Assurance (QA) is another broader term that includes quality of processes. Configuration audits add more scope. In parallel there are some less visible dimensions in quality not often addressed in traditional models such as business alignment of QA efforts. This paper compares the commonly accepted models related to software quality management and proposes a model that fills an empty space in this area. The paper provides some analysis of the concepts of maturity and capability levels and provides some proposed adaptations for quality management assessment.

2017-05-17
Dutt, Nikil, Jantsch, Axel, Sarma, Santanu.  2016.  Toward Smart Embedded Systems: A Self-aware System-on-Chip (SoC) Perspective. ACM Trans. Embed. Comput. Syst.. 15:22:1–22:27.

Embedded systems must address a multitude of potentially conflicting design constraints such as resiliency, energy, heat, cost, performance, security, etc., all in the face of highly dynamic operational behaviors and environmental conditions. By incorporating elements of intelligence, the hope is that the resulting “smart” embedded systems will function correctly and within desired constraints in spite of highly dynamic changes in the applications and the environment, as well as in the underlying software/hardware platforms. Since terms related to “smartness” (e.g., self-awareness, self-adaptivity, and autonomy) have been used loosely in many software and hardware computing contexts, we first present a taxonomy of “self-x” terms and use this taxonomy to relate major “smart” software and hardware computing efforts. A major attribute for smart embedded systems is the notion of self-awareness that enables an embedded system to monitor its own state and behavior, as well as the external environment, so as to adapt intelligently. Toward this end, we use a System-on-Chip perspective to show how the CyberPhysical System-on-Chip (CPSoC) exemplar platform achieves self-awareness through a combination of cross-layer sensing, actuation, self-aware adaptations, and online learning. We conclude with some thoughts on open challenges and research directions.

2017-04-20
You, T..  2016.  Toward the future of internet architecture for IoE: Precedent research on evolving the identifier and locator separation schemes. 2016 International Conference on Information and Communication Technology Convergence (ICTC). :436–439.

Internet has been being becoming the most famous and biggest communication networks as social, industrial, and public infrastructure since Internet was invented at late 1960s. In a historical retrospect of Internet's evolution, the Internet architecture continues evolution repeatedly by going through various technical challenges, for instance, in early 1990s, Internet had encountered danger of scalability, after a short while it had been overcome and successfully evolved by applying emerging techniques such as CIDR, NAT, and IPv6. Especially this paper emphasizes scalability issues as technical challenges with forecasting that Internet of things era has come. Firstly, we describe the Identifier and locator separation scheme that can achieve dramatically architectural evolution in historical perspective. Additionally, it reviews various kinds of Identifier and locator separation scheme because recently the scheme can be the major design pillar towards future of Internet architecture such as both various clean-slated future Internet architectures and evolving Internet architectures. Lastly we show a result of analysis by analysis table for future of internet of everything where number of Internet connected devices will growth to more than 20 billion by 2020.

2017-04-24
Miao, Luwen, Liu, Kaikai.  2016.  Towards a Heterogeneous Internet-of-Things Testbed via Mesh Inside a Mesh: Poster Abstract. Proceedings of the 14th ACM Conference on Embedded Network Sensor Systems CD-ROM. :368–369.

Connectivity is at the heart of the future Internet-of-Things (IoT) infrastructure, which can control and communicate with remote sensors and actuators for the beacons, data collections, and forwarding nodes. Existing sensor network solutions cannot solve the bottleneck problems near the sink node; the tree-based Internet architecture has the single point of failure. To solve current deficiencies in multi-hop mesh network and cross-domain network design, we propose a mesh inside a mesh IoT network architecture. Our designed "edge router" incorporates these two mesh networks together and performs seamlessly transmission of multi-standard packets. The proposed IoT testbed interoperates with existing multi-standards (Wi-Fi, 6LoWPAN) and segments of networks, and provides both high-throughput Internet and resilient sensor coverage throughout the community.

2017-04-20
McCall, Roderick, McGee, Fintan, Meschtscherjakov, Alexander, Louveton, Nicolas, Engel, Thomas.  2016.  Towards A Taxonomy of Autonomous Vehicle Handover Situations. Proceedings of the 8th International Conference on Automotive User Interfaces and Interactive Vehicular Applications. :193–200.

This paper proposes a taxonomy of autonomous vehicle handover situations with a particular emphasis on situational awareness. It focuses on a number of research challenges such as: legal responsibility, the situational awareness level of the driver and the vehicle, the knowledge the vehicle must have of the driver's driving skills as well as the in-vehicle context. The taxonomy acts as a starting point for researchers and practitioners to frame the discussion on this complex problem.

2017-05-30
Shah, Anant, Fontugne, Romain, Papadopoulos, Christos.  2016.  Towards Characterizing International Routing Detours. Proceedings of the 12th Asian Internet Engineering Conference. :17–24.

There are currently no requirements (technical or otherwise) that routing paths must be contained within national boundaries. Indeed, some paths experience international detours, i.e., originate in one country, cross international boundaries and return to the same country. In most cases these are sensible traffic engineering or peering decisions at ISPs that serve multiple countries. In some cases such detours may be suspicious. Characterizing international detours is useful to a number of players: (a) network engineers trying to diagnose persistent problems, (b) policy makers aiming at adhering to certain national communication policies, (c) entrepreneurs looking for opportunities to deploy new networks, or (d) privacy-conscious states trying to minimize the amount of internal communication traversing different jurisdictions. In this paper we characterize international detours in the Internet during the month of January 2016. To detect detours we sample BGP RIBs every 8 hours from 461 RouteViews and RIPE RIS peers spanning 30 countries. We use geolocation of ASes which geolocates each BGP prefix announced by each AS, mapping its presence at IXPs and geolocation infrastructure IPs. Finally, we analyze each global BGP RIB entry looking for detours. Our analysis shows more than 5K unique BGP prefixes experienced a detour. 132 prefixes experienced more than 50% of the detours. We observe about 544K detours. Detours either last for a few days or persist the entire month. Out of all the detours, more than 90% were transient detours that lasted for 72 hours or less. We also show different countries experience different characteristics of detours.

2017-05-18
Wang, Huangxin, Li, Fei, Chen, Songqing.  2016.  Towards Cost-Effective Moving Target Defense Against DDoS and Covert Channel Attacks. Proceedings of the 2016 ACM Workshop on Moving Target Defense. :15–25.

Traditionally, network and system configurations are static. Attackers have plenty of time to exploit the system's vulnerabilities and thus they are able to choose when to launch attacks wisely to maximize the damage. An unpredictable system configuration can significantly lift the bar for attackers to conduct successful attacks. Recent years, moving target defense (MTD) has been advocated for this purpose. An MTD mechanism aims to introduce dynamics to the system through changing its configuration continuously over time, which we call adaptations. Though promising, the dynamic system reconfiguration introduces overhead to the applications currently running in the system. It is critical to determine the right time to conduct adaptations and to balance the overhead afforded and the security levels guaranteed. This problem is known as the MTD timing problem. Little prior work has been done to investigate the right time in making adaptations. In this paper, we take the first step to both theoretically and experimentally study the timing problem in moving target defenses. For a broad family of attacks including DDoS attacks and cloud covert channel attacks, we model this problem as a renewal reward process and propose an optimal algorithm in deciding the right time to make adaptations with the objective of minimizing the long-term cost rate. In our experiments, both DDoS attacks and cloud covert channel attacks are studied. Simulations based on real network traffic traces are conducted and we demonstrate that our proposed algorithm outperforms known adaptation schemes.

2017-03-20
Malecha, Gregory, Ricketts, Daniel, Alvarez, Mario M., Lerner, Sorin.  2016.  Towards foundational verification of cyber-physical systems. :1–5.

The safety-critical aspects of cyber-physical systems motivate the need for rigorous analysis of these systems. In the literature this work is often done using idealized models of systems where the analysis can be carried out using high-level reasoning techniques such as Lyapunov functions and model checking. In this paper we present VERIDRONE, a foundational framework for reasoning about cyber-physical systems at all levels from high-level models to C code that implements the system. VERIDRONE is a library within the Coq proof assistant enabling us to build on its foundational implementation, its interactive development environments, and its wealth of libraries capturing interesting theories ranging from real numbers and differential equations to verified compilers and floating point numbers. These features make proof assistants in general, and Coq in particular, a powerful platform for unifying foundational results about safety-critical systems and ensuring interesting properties at all levels of the stack.

Malecha, Gregory, Ricketts, Daniel, Alvarez, Mario M., Lerner, Sorin.  2016.  Towards foundational verification of cyber-physical systems. :1–5.

The safety-critical aspects of cyber-physical systems motivate the need for rigorous analysis of these systems. In the literature this work is often done using idealized models of systems where the analysis can be carried out using high-level reasoning techniques such as Lyapunov functions and model checking. In this paper we present VERIDRONE, a foundational framework for reasoning about cyber-physical systems at all levels from high-level models to C code that implements the system. VERIDRONE is a library within the Coq proof assistant enabling us to build on its foundational implementation, its interactive development environments, and its wealth of libraries capturing interesting theories ranging from real numbers and differential equations to verified compilers and floating point numbers. These features make proof assistants in general, and Coq in particular, a powerful platform for unifying foundational results about safety-critical systems and ensuring interesting properties at all levels of the stack.