Biblio

Found 2688 results

Filters: First Letter Of Last Name is P  [Clear All Filters]
2019-02-25
Cayetano, Trisha Anne, Dogao, Averyl, Guipoc, Cristopher, Palaoag, Thelma.  2018.  Cyber-Physical IT Assessment Tool and Vulnerability Assessment for Semiconductor Companies. Proceedings of the 2Nd International Conference on Cryptography, Security and Privacy. :67–71.

Information and systems are the most valuable asset of almost all global organizations. Thus, sufficient security is key to protect these assets. The reliability and security of a manufacturing company's supply chain are key concerns as it manages assurance & quality of supply. Traditional concerns such as physical security, disasters, political issues & counterfeiting remain, but cyber security is an area of growing interest. Statistics show that cyber-attacks still continue with no signs of slowing down. Technical controls, no matter how good, will only take the company thus far since no usable system is 100 percent secure or impenetrable. Evaluating the security vulnerabilities of one organization and taking the action to mitigate the risks will strengthen the layer of protection in the manufacturing company's supply chain. In this paper, the researchers created an IT Security Assessment Tool to facilitate the evaluation of the sufficiency of policy, procedures, and controls implemented by semiconductor companies. The proposed IT Security Assessment Tool was developed considering the factors that are critical in protecting the information and systems of various semiconductor companies. Subsequently, the created IT Security Assessment Tool was used to evaluate existing semiconductor companies to identify their areas of security vulnerabilities. The result shows that all suppliers visited do not have cyber security programs and most dwell on physical and network security controls. Best practices were shared and action items were suggested to improve the security controls and minimize risk of service disruption for customers, theft of sensitive data and reputation damage.

2019-06-24
Bessa, Ricardo J., Rua, David, Abreu, Cláudia, Machado, Paulo, Andrade, José R., Pinto, Rui, Gonçalves, Carla, Reis, Marisa.  2018.  Data Economy for Prosumers in a Smart Grid Ecosystem. Proceedings of the Ninth International Conference on Future Energy Systems. :622–630.

Smart grids technologies are enablers of new business models for domestic consumers with local flexibility (generation, loads, storage) and where access to data is a key requirement in the value stream. However, legislation on personal data privacy and protection imposes the need to develop local models for flexibility modeling and forecasting and exchange models instead of personal data. This paper describes the functional architecture of an home energy management system (HEMS) and its optimization functions. A set of data-driven models, embedded in the HEMS, are discussed for improving renewable energy forecasting skill and modeling multi-period flexibility of distributed energy resources.

Wang, J., Zhang, X., Zhang, H., Lin, H., Tode, H., Pan, M., Han, Z..  2018.  Data-Driven Optimization for Utility Providers with Differential Privacy of Users' Energy Profile. 2018 IEEE Global Communications Conference (GLOBECOM). :1–6.

Smart meters migrate conventional electricity grid into digitally enabled Smart Grid (SG), which is more reliable and efficient. Fine-grained energy consumption data collected by smart meters helps utility providers accurately predict users' demands and significantly reduce power generation cost, while it imposes severe privacy risks on consumers and may discourage them from using those “espionage meters". To enjoy the benefits of smart meter measured data without compromising the users' privacy, in this paper, we try to integrate distributed differential privacy (DDP) techniques into data-driven optimization, and propose a novel scheme that not only minimizes the cost for utility providers but also preserves the DDP of users' energy profiles. Briefly, we add differential private noises to the users' energy consumption data before the smart meters send it to the utility provider. Due to the uncertainty of the users' demand distribution, the utility provider aggregates a given set of historical users' differentially private data, estimates the users' demands, and formulates the data- driven cost minimization based on the collected noisy data. We also develop algorithms for feasible solutions, and verify the effectiveness of the proposed scheme through simulations using the simulated energy consumption data generated from the utility company's real data analysis.

2019-10-30
Demoulin, Henri Maxime, Vaidya, Tavish, Pedisich, Isaac, DiMaiolo, Bob, Qian, Jingyu, Shah, Chirag, Zhang, Yuankai, Chen, Ang, Haeberlen, Andreas, Loo, Boon Thau et al..  2018.  DeDoS: Defusing DoS with Dispersion Oriented Software. Proceedings of the 34th Annual Computer Security Applications Conference. :712-722.

This paper presents DeDoS, a novel platform for mitigating asymmetric DoS attacks. These attacks are particularly challenging since even attackers with limited resources can exhaust the resources of well-provisioned servers. DeDoS offers a framework to deploy code in a highly modular fashion. If part of the application stack is experiencing a DoS attack, DeDoS can massively replicate only the affected component, potentially across many machines. This allows scaling of the impacted resource separately from the rest of the application stack, so that resources can be precisely added where needed to combat the attack. Our evaluation results show that DeDoS incurs reasonable overheads in normal operations, and that it significantly outperforms standard replication techniques when defending against a range of asymmetric attacks.

2019-11-12
Padon, Oded.  2018.  Deductive Verification of Distributed Protocols in First-Order Logic. 2018 Formal Methods in Computer Aided Design (FMCAD). :1-1.

Formal verification of infinite-state systems, and distributed systems in particular, is a long standing research goal. In the deductive verification approach, the programmer provides inductive invariants and pre/post specifications of procedures, reducing the verification problem to checking validity of logical verification conditions. This check is often performed by automated theorem provers and SMT solvers, substantially increasing productivity in the verification of complex systems. However, the unpredictability of automated provers presents a major hurdle to usability of these tools. This problem is particularly acute in case of provers that handle undecidable logics, for example, first-order logic with quantifiers and theories such as arithmetic. The resulting extreme sensitivity to minor changes has a strong negative impact on the convergence of the overall proof effort.

2020-10-05
Lago, Loris Dal, Ferrante, Orlando, Passerone, Roberto, Ferrari, Alberto.  2018.  Dependability Assessment of SOA-Based CPS With Contracts and Model-Based Fault Injection. IEEE Transactions on Industrial Informatics. 14:360—369.

Engineering complex distributed systems is challenging. Recent solutions for the development of cyber-physical systems (CPS) in industry tend to rely on architectural designs based on service orientation, where the constituent components are deployed according to their service behavior and are to be understood as loosely coupled and mostly independent. In this paper, we develop a workflow that combines contract-based and CPS model-based specifications with service orientation, and analyze the resulting model using fault injection to assess the dependability of the systems. Compositionality principles based on the contract specification help us to make the analysis practical. The presented techniques are evaluated on two case studies.

2018-09-30
Arjen van der Meer, Cornelius Steinbrink, Kai Heussen, Daniel E. Morales Bondy, Merkebu Z. Degefa, Filip Pröstl Andrén, Thomas Strasser, Sebastian Lehnhoff, Peter Palensky.  2018.  Design of experiments aided holistic testing of cyber-physical energy systems. 2018 Workshop on Modeling and Simulation of Cyber-Physical Energy Systems (MSCPES). :1–7.

The complex and often safety-critical nature of cyber-physical energy systems makes validation a key challenge in facilitating the energy transition, especially when it comes to the testing on system level. Reliable and reproducible validation experiments can be guided by the concept of design of experiments, which is, however, so far not fully adopted by researchers. This paper suggests a structured guideline for design of experiments application within the holistic testing procedure suggested by the European ERIGrid project. In this paper, a general workflow as well as a practical example are provided with the aim to give domain experts a basic understanding of design of experiments compliant testing.

2019-01-31
Buhren, Robert, Hetzelt, Felicitas, Pirnay, Niklas.  2018.  On the Detectability of Control Flow Using Memory Access Patterns. Proceedings of the 3rd Workshop on System Software for Trusted Execution. :48–53.

Shielding systems such as AMD's Secure Encrypted Virtualization aim to protect a virtual machine from a higher privileged entity such as the hypervisor. A cornerstone of these systems is the ability to protect the memory from unauthorized accesses. Despite this protection mechanism, previous attacks leveraged the control over memory resources to infer control flow of applications running in a shielded system. While previous works focused on a specific target application, there has been no general analysis on how the control flow of a protected application can be inferred. This paper tries to overcome this gap by providing a detailed analysis on the detectability of control flow using memory access patterns. To that end, we do not focus on a specific shielding system or a specific target application, but present a framework which can be applied to different types of shielding systems as well as to different types of attackers. By training a random forest classifier on the memory accesses emitted by syscalls of a shielded entity, we show that it is possible to infer the control flow of shielded entities with a high degree of accuracy.

2019-10-15
Panagiotakis, C., Papadakis, H., Fragopoulou, P..  2018.  Detection of Hurriedly Created Abnormal Profiles in Recommender Systems. 2018 International Conference on Intelligent Systems (IS). :499–506.

Recommender systems try to predict the preferences of users for specific items. These systems suffer from profile injection attacks, where the attackers have some prior knowledge of the system ratings and their goal is to promote or demote a particular item introducing abnormal (anomalous) ratings. The detection of both cases is a challenging problem. In this paper, we propose a framework to spot anomalous rating profiles (outliers), where the outliers hurriedly create a profile that injects into the system either random ratings or specific ratings, without any prior knowledge of the existing ratings. The proposed detection method is based on the unpredictable behavior of the outliers in a validation set, on the user-item rating matrix and on the similarity between users. The proposed system is totally unsupervised, and in the last step it uses the k-means clustering method automatically spotting the spurious profiles. For the cases where labeling sample data is available, a random forest classifier is trained to show how supervised methods outperforms unsupervised ones. Experimental results on the MovieLens 100k and the MovieLens 1M datasets demonstrate the high performance of the proposed schemata.

2019-04-29
Kar, Diptendu Mohan, Ray, Indrajit, Gallegos, Jenna, Peccoud, Jean.  2018.  Digital Signatures to Ensure the Authenticity and Integrity of Synthetic DNA Molecules. Proceedings of the New Security Paradigms Workshop. :110–122.

DNA synthesis has become increasingly common, and many synthetic DNA molecules are licensed intellectual property (IP). DNA samples are shared between academic labs, ordered from DNA synthesis companies and manipulated for a variety of different purposes, mostly to study their properties and improve upon them. However, it is not uncommon for a sample to change hands many times with very little accompanying information and no proof of origin. This poses significant challenges to the original inventor of a DNA molecule, trying to protect her IP rights. More importantly, following the anthrax attacks of 2001, there is an increased urgency to employ microbial forensic technologies to trace and track agent inventories. However, attribution of physical samples is next to impossible with existing technologies. In this paper, we describe our efforts to solve this problem by embedding digital signatures in DNA molecules synthesized in the laboratory. We encounter several challenges that we do not face in the digital world. These challenges arise primarily from the fact that changes to a physical DNA molecule can affect its properties, random mutations can accumulate in DNA samples over time, DNA sequencers can sequence (read) DNA erroneously and DNA sequencing is still relatively expensive (which means that laboratories would prefer not to read and re-read their DNA samples to get error-free sequences). We address these challenges and present a digital signature technology that can be applied to synthetic DNA molecules in living cells.

2019-01-21
Ghafir, Ibrahim, Prenosil, Vaclav, Hammoudeh, Mohammad, Aparicio-Navarro, Francisco J., Rabie, Khaled, Jabban, Ahmad.  2018.  Disguised Executable Files in Spear-phishing Emails: Detecting the Point of Entry in Advanced Persistent Threat. Proceedings of the 2Nd International Conference on Future Networks and Distributed Systems. :44:1–44:5.

In recent years, cyber attacks have caused substantial financial losses and been able to stop fundamental public services. Among the serious attacks, Advanced Persistent Threat (APT) has emerged as a big challenge to the cyber security hitting selected companies and organisations. The main objectives of APT are data exfiltration and intelligence appropriation. As part of the APT life cycle, an attacker creates a Point of Entry (PoE) to the target network. This is usually achieved by installing malware on the targeted machine to leave a back-door open for future access. A common technique employed to breach into the network, which involves the use of social engineering, is the spear phishing email. These phishing emails may contain disguised executable files. This paper presents the disguised executable file detection (DeFD) module, which aims at detecting disguised exe files transferred over the network connections. The detection is based on a comparison between the MIME type of the transferred file and the file name extension. This module was experimentally evaluated and the results show a successful detection of disguised executable files.

2019-02-22
Poovendran, Radha.  2018.  Dynamic Defense Against Adaptive and Persistent Adversaries. Proceedings of the 5th ACM Workshop on Moving Target Defense. :57-58.

This talk will cover two topics, namely, modeling and design of Moving Target Defense (MTD), and DIFT games for modeling Advanced Persistent Threats (APTs). We will first present a game-theoretic approach to characterizing the trade-off between resource efficiency and defense effectiveness in decoy- and randomization-based MTD. We will then address the game formulation for APTs. APTs are mounted by intelligent and resourceful adversaries who gain access to a targeted system and gather information over an extended period of time. APTs consist of multiple stages, including initial system compromise, privilege escalation, and data exfiltration, each of which involves strategic interaction between the APT and the targeted system. While this interaction can be viewed as a game, the stealthiness, adaptiveness, and unpredictability of APTs imply that the information structure of the game and the strategies of the APT are not readily available. Our approach to modeling APTs is based on the insight that the persistent nature of APTs creates information flows in the system that can be monitored. One monitoring mechanism is Dynamic Information Flow Tracking (DIFT), which taints and tracks malicious information flows through a system and inspects the flows at designated traps. Since tainting all flows in the system will incur significant memory and storage overhead, efficient tagging policies are needed to maximize the probability of detecting the APT while minimizing resource costs. In this work, we develop a multi-stage stochastic game framework for modeling the interaction between an APT and a DIFT, as well as designing an efficient DIFT-based defense. Our model is grounded on APT data gathered using the Refinable Attack Investigation (RAIN) flow-tracking framework. We present the current state of our formulation, insights that it provides on designing effective defenses against APTs, and directions for future work.

2020-01-07
Akiwate, Bahubali, Parthiban, Latha.  2018.  A Dynamic DNA for Key-Based Cryptography. 2018 International Conference on Computational Techniques, Electronics and Mechanical Systems (CTEMS). :223-227.

A dynamic DNA for key-based Cryptography that encrypt and decrypt plain text characters, text file, image file and audio file using DNA sequences. Cryptography is always taken as the secure way while transforming the confidential information over the network such as LAN, Internet. But over the time, the traditional cryptographic approaches are been replaced with more effective cryptographic systems such as Quantum Cryptography, Biometric Cryptography, Geographical Cryptography and DNA Cryptography. This approach accepts the DNA sequences as the input to generate the key that going to provide two stages of data security.

2019-11-26
Pulungan, Farid Fajriana, Sudiharto, Dodi Wisaksono, Brotoharsono, Tri.  2018.  Easy Secure Login Implementation Using Pattern Locking and Environmental Context Recognition. 2018 International Conference on Applied Engineering (ICAE). :1-6.

Smartphone has become the tool which is used daily in modern human life. Some activities in human life, according to the usage of the smartphone can be related to the information which has a high privilege and needs a privacy. It causes the owners of the smartphone needs a system which can protect their privacy. Unfortunately, the secure the system, the unease of the usage. Hence, the system which has an invulnerable environment but also gives the ease of use is very needful. The aspect which is related to the ease of use is an authentication mechanism. Sometimes, this aspect correspondence to the effectiveness and the efficiency. This study is going to analyze the application related to this aspect which is a lock screen application. This lock screen application uses the context data based on the environment condition around the user. The context data used are GPS location and Mac Address of Wi-Fi. The system is going to detect the context and is going to determine if the smartphone needs to run the authentication mechanism or to bypass it based on the analysis of the context data. Hopefully, the smartphone application which is developed still can provide mobility and usability features, and also can protect the user privacy even though it is located in the environment which its context data is unknown.

2019-09-26
Pfeffer, T., Herber, P., Druschke, L., Glesner, S..  2018.  Efficient and Safe Control Flow Recovery Using a Restricted Intermediate Language. 2018 IEEE 27th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). :235-240.

Approaches for the automatic analysis of security policies on source code level cannot trivially be applied to binaries. This is due to the lacking high-level semantics of low-level object code, and the fundamental problem that control-flow recovery from binaries is difficult. We present a novel approach to recover the control-flow of binaries that is both safe and efficient. The key idea of our approach is to use the information contained in security mechanisms to approximate the targets of computed branches. To achieve this, we first define a restricted control transition intermediate language (RCTIL), which restricts the number of possible targets for each branch to a finite number of given targets. Based on this intermediate language, we demonstrate how a safe model of the control flow can be recovered without data-flow analyses. Our evaluation shows that that makes our solution more efficient than existing solutions.

2019-01-31
Agarkhed, Jayashree, R, Ashalatha., Patil, Siddarama R..  2018.  An Efficient Privacy Preserving Cryptographic Approach in Cloud Computing. Proceedings of the 2Nd International Conference on Future Networks and Distributed Systems. :42:1–42:10.

Cloud computing belongs to distributed network technology for computing and storage capabilities purpose. It is a kind of cost-effective technology dedicated to information technology. Using the Internet, the accessibility and retrieving of cloud data have become much more accessible. The service providers can expand the storage space in a cloud environment. Security is well-thought-out to be the essential attribute in a distributed system. Cryptography can be described as a method of securing the data from attackers and eavesdroppers. Third Party Auditor is responsible for the authentication of secret files in cloud system on behalf of the data owner. The data auditability technique allows the user to make the data integrity check using a third party. Cloud computing offers unlimited data space for storage to its users and also serves sharing of data and planned use of heterogeneous resources in distributed systems. This paper describes privacy-preserving enabled public auditing method using cryptographic techniques for low-performance based end devices.

2019-12-16
Peguero, Ksenia, Zhang, Nan, Cheng, Xiuzhen.  2018.  An Empirical Study of the Framework Impact on the Security of JavaScript Web Applications. Companion Proceedings of the The Web Conference 2018. :753–758.

\textbackslashtextbackslashtextitBackground: JavaScript frameworks are widely used to create client-side and server-side parts of contemporary web applications. Vulnerabilities like cross-site scripting introduce significant risks in web applications.\textbackslashtextbackslash\textbackslashtextbackslash \textbackslashtextbackslashtextitAim: The goal of our study is to understand how the security features of a framework impact the security of the applications written using that framework.\textbackslashtextbackslash\textbackslashtextbackslash \textbackslashtextbackslashtextitMethod: In this paper, we present four locations in an application, relative to the framework being used, where a mitigation can be applied. We perform an empirical study of JavaScript applications that use the three most common template engines: Jade/Pug, EJS, and Angular. Using automated and manual analysis of each group of applications, we identify the number of projects vulnerable to cross-site scripting, and the number of vulnerabilities in each project, based on the framework used.\textbackslashtextbackslash\textbackslashtextbackslash \textbackslashtextbackslashtextitResults: We analyze the results to compare the number of vulnerable projects to the mitigation locations used in each framework and perform statistical analysis of confounding variables.\textbackslashtextbackslash\textbackslashtextbackslash \textbackslashtextbackslashtextitConclusions: The location of the mitigation impacts the application's security posture, with mitigations placed within the framework resulting in more secure applications.

2019-06-28
Park, Younghee, Hu, Hongxin, Yuan, Xiaohong, Li, Hongda.  2018.  Enhancing Security Education Through Designing SDN Security Labs in CloudLab. Proceedings of the 49th ACM Technical Symposium on Computer Science Education. :185-190.

Software-Defined Networking (SDN) represents a major shift from ossified hardware-based networks to programmable software-based networks. It introduces significant granularity, visibility, and flexibility into networking, but at the same time brings new security challenges. Although the research community is making progress in addressing both the opportunities in SDN and the accompanying security challenges, very few educational materials have been designed to incorporate the latest research results and engage students in learning about SDN security. In this paper, we presents our newly designed SDN security education materials, which can be used to meet the ever-increasing demand for high quality cybersecurity professionals with expertise in SDN security. The designed security education materials incorporate the latest research results in SDN security and are integrated into CloudLab, an open cloud platform, for effective hands-on learning. Through a user study, we demonstrate that students have a better understanding of SDN security after participating in these well-designed CloudLab-based security labs, and they also acquired strong research interests in SDN security.

2019-02-22
Pevny, Tomas, Ker, Andrew D..  2018.  Exploring Non-Additive Distortion in Steganography. Proceedings of the 6th ACM Workshop on Information Hiding and Multimedia Security. :109-114.

Leading steganography systems make use of the Syndrome-Trellis Code (STC) algorithm to minimize a distortion function while encoding the desired payload, but this constrains the distortion function to be additive. The Gibbs Embedding algorithm works for a certain class of non-additive distortion functions, but has its own limitations and is highly complex. In this short paper we show that it is possible to modify the STC algorithm in a simple way, to minimize a non-additive distortion function suboptimally. We use it for two examples. First, applying it to the S-UNIWARD distortion function, we show that it does indeed reduce distortion, compared with minimizing the additive approximation currently used in image steganography, but that it makes the payload more – not less – detectable. This parallels research attempting to use Gibbs Embedding for the same task. Second, we apply it to distortion defined by the output of a specific detector, as a counter-move in the steganography game. However, unless the Warden is forced to move first (by fixing the detector) this is highly detectable.

2018-05-15
Pratap Bhanu Solanki, Xiaobo Tan.  2018.  Extended Kalman filter-based 3D active-alignment control for LED communication. Proceedings of 2018 IEEE International Conference on Robotics and Automation. :5476-5481.

Under review

2018-10-26
Brokalakis, A., Chondroulis, I., Papaefstathiou, I..  2018.  Extending the Forward Error Correction Paradigm for Multi-Hop Wireless Sensor Networks. 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS). :1–5.

In typical Wireless Sensor Network (WSN) applications, the sensor nodes deployed are constrained both in computational and energy resources. For this reason, simple communication protocols are usually employed along with shortrange multi-hop topologies. In this paper, we challenge this notion and propose a structure that employs more robust (and naturally more complex) forward-error correction schemes in multi-hop extended star topologies. We demonstrate using simulation and real-world data based on popular WSN platforms that this approach can actually reduce the overall energy consumption of the nodes by significant margins (from 40 to 70%) compared to traditional WSN schemes that do not support sophisticated communication mechanisms and it is feasible to implement it economically without relying on expensive hardware.

2019-01-31
Lyu, C., Pande, A., Zhang, Y., Gu, D., Mohapatra, P..  2018.  FastTrust: Fast and Anonymous Spatial-Temporal Trust for Connected Cars on Expressways. 2018 15th Annual IEEE International Conference on Sensing, Communication, and Networking (SECON). :1–9.

Connected cars have received massive attention in Intelligent Transportation System. Many potential services, especially safety-related ones, rely on spatial-temporal messages periodically broadcast by cars. Without a secure authentication algorithm, malicious cars may send out invalid spatial-temporal messages and then deny creating them. Meanwhile, a lot of private information may be disclosed from these spatial-temporal messages. Since cars move on expressways at high speed, any authentication must be performed in real-time to prevent crashes. In this paper, we propose a Fast and Anonymous Spatial-Temporal Trust (FastTrust) mechanism to ensure these properties. In contrast to most authentication protocols which rely on fixed infrastructures, FastTrust is distributed and mostly designed on symmetric-key cryptography and an entropy-based commitment, and is able to fast authenticate spatial-temporal messages. FastTrust also ensures the anonymity and unlinkability of spatial-temporal messages by developing a pseudonym-varying scheduling scheme on cars. We provide both analytical and simulation evaluations to show that FastTrust achieves the security and privacy properties. FastTrust is low-cost in terms of communication and computational resources, authenticating 20 times faster than existing Elliptic Curve Digital Signature Algorithm.

2019-03-22
Pahariya, Parth, Singh, Sanjay Kumar.  2018.  Fingerprint Authentication Using LT Codes. Proceedings of the 2018 2Nd International Conference on Biometric Engineering and Applications. :38-42.

Biometric is used for identifying the person based on their traits. Fingerprint is one of the most important and most used biometric trait for person authentication. Fingerprint database must be stored in efficient way and in most secure way so that it is unable to hack by the hacker and it will be able to recognize the person fast in large database. In this paper, we proposed an efficient way of storing the fingerprint data for fast recognition. We are using LT codes for storing the x coordinates of minutiae points and fingerprint images is stored in encrypted form with the coordinates. We are using on-the-y gaussian algorithm for decoding the x coordinates and calculate the value for finding similarity in between two fingerprints.

2019-06-28
Park, Daejun, Zhang, Yi, Saxena, Manasvi, Daian, Philip, Ro\c su, Grigore.  2018.  A Formal Verification Tool for Ethereum VM Bytecode. Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. :912-915.

In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.

2019-08-28
Patricia Hidalgo-Gonzalez, Roel Dobbe, Rodrigo Henriquez-Auba, Duncan Callaway, Claire Tomlin.  2018.  Frequency Regulation in Hybrid Power Dynamics with Variable and Low Inertia due to Renewable Energy. 57th IEEE Conference on Decision and Control.

As more non-synchronous renewable energy sources (RES) participate in power systems, the system's inertia decreases and becomes time dependent, challenging the ability of existing control schemes to maintain frequency stability. System operators, research laboratories, and academic institutes have expressed the importance to adapt to this new power system paradigm. As one of the potential solutions, virtual inertia has become an active research area. However, power dynamics have been modeled as time-invariant, by not modeling the variability in the system's inertia. To address this, we propose a new modeling framework for power system dynamics to simulate a time-varying evolution of rotational inertia coefficients in a network. We model power dynamics as a hybrid system with discrete modes representing different rotational inertia regimes of the network. We test the performance of two classical controllers from the literature in this new hybrid modeling framework: optimal closed-loop Model Predictive Control (MPC) and virtual inertia placement. Results show that the optimal closed-loop MPC controller (Linear MPC) performs the best in terms of cost; it is 82 percent less expensive than virtual inertia placement. It is also more efficient in terms of energy injected/absorbed to control frequency. To address the lower performance of virtual inertia placement, we then propose a new Dynamic Inertia Placement scheme and we find that it is more efficient in terms of cost (74 percent cheaper) and energy usage, compared to classical inertia placement schemes from the literature.