@article{, author = {Dantas, Yuri Gil and Munaro, Tiziano and C{\^{a}}rlan, Carmen and Nigam, Vivek and Barner, Simon and Fan, Shiqing and Pretschner, Alexander and Sch{\"{o}}pp, Ulrich and Tverdyshev, Sergey}, title = {A Toolchain for Synthesizing and Validating Safety Architectures}, publisher = {Springer}, journal = {SN Computer Science}, volume = {4}, number = {4}, pages = {335}, year = {2023}, month = apr, timestamp = 2023.04.15, abstract = {Autonomous vehicles handle complicated tasks that may lead to harm when performed incorrectly. These harms, in particular when caused by system faults, may be avoided by the deployment of safety architectural patterns, such as the Heterogeneous Duplex pattern. Our goal is to provide safety engineers with computer-aided support for synthesizing architectures with safety architecture patterns. To this end, we build on our previous work in which we proposed a model-based system engineering plugin to enable the model-driven approach using safety architecture patterns. This article proposes a toolchain for synthesizing the structure and switching logic of safety architectures, as well as for validating them through simulation-based fault-injection. We validate our toolchain using an industrial use-case for autonomous driving systems, namely, a Highway Pilot system.}, issn = {2661-8907}, doi = {10.1007/s42979-023-01712-5}, keywords = {Model-based systems engineering, Toolchain, Safety architecture patterns, Reconfiguration, Simulation, MbSE, AutoFOCUS3, DSE}, } @inproceedings{, author = {Terzimehić, Tarik and Barner, Simon and Dantas, Yuri Gil and Sch{\"{o}}pp, Ulrich and Nigam, Vivek and Ke, Pei}, title = {Safety-Aware Deployment Synthesis and Trade-Off Analysis of Apollo Autonomous Driving Platform}, booktitle = {9th International Workshop on Automotive System/Software Architectures ({WASA}) co-located with {ICSA} 2023}, publisher = {IEEE}, year = {2023}, month = mar, abstract = {The adoption of autonomous cars requires operational critical functions even in the event of HW faults and/or SW defects, and protection of safety-critical functions against security threats. Defining appropriate safe and secure architectures is challenging and costly. In previous work, we have proposed tools to automate the recommendation of safety and security patterns for safety-critical systems. However, safety and security measures may (negatively) influence system performance, besides introducing additional development effort. We present a design space exploration approach, a model-based engineering workflow and tool prototype for automated guidance on trade-off decisions when applying safety and security patterns on a given (unsafe) baseline architecture. Based on models that abstract the vehicle’s functionality and its software and hardware components, as well as an engine for the automated pattern recommendation, we investigate the optimization of HW/SW deployments, and provide a trade-off analysis for different architecture candidates. We implemented our approach in an open-source tool and evaluate it with a model of the Apollo autonomous driving platform.}, doi = {10.1109/ICSA-C57050.2023.00070}, keywords = {Autonomous vehicles, Apollo, model-driven development, system architecture, safety, model-based systems engineering, MbSE, design-space exploration, DSE, AutoFOCUS3, AF3}, } @article{tcps2022, author = {Dantas, Yuri Gil and Nigam, Vivek}, title = {Automating Safety and Security Co-Design through Semantically-Rich Architecture Patterns}, publisher = {ACM}, journal = {Transactions on Cyber-Physical Systems}, volume = {7}, number = {1}, year = {2023}, month = feb, abstract = {During the design of safety-critical systems, safety and security engineers make use of architecture patterns, such as Watchdog and Firewall, to address identified failures and threats. Often, however, the deployment of safety architecture patterns has consequences on security; e.g., the deployment of a safety architecture pattern may lead to new threats. The other way around may also be possible; i.e., the deployment of a security architecture pattern may lead to new failures. Safety and security co-design is, therefore, required to understand such consequences and tradeoffs in order to reach appropriate system designs. Currently, architecture pattern descriptions, including their consequences, are described using natural language. Therefore, their deployment in system design is carried out manually by experts and thus is time-consuming and prone to human error, especially given the high system complexity. We propose the use of semantically rich architecture patterns to enable automated support for safety and security co-design by using Knowledge Representation and Reasoning (KRR) methods. Based on our domain-specific language, we specify reasoning principles as logic specifications written as answer-set programs. KRR engines enable the automation of safety and security co-engineering activities, including the automated recommendation of which architecture patterns can address failures or threats, and consequences of deploying such patterns. We demonstrate our approach on an example taken from the ISO 21434 standard.}, doi = {10.1145/3565269}, } @inproceedings{icissp23_1, author = {Dantas, Yuri Gil and Nigam, Vivek and Sch{\"{o}}pp, Ulrich and Barner, Simon and Ke, Pei}, title = {Automating Vehicle SOA Threat Analysis using a Model-Based Methodology}, booktitle = {Proceedings of the 9th International Conference on Information Systems Security and Privacy (ICISSP)}, publisher = {SciTePress}, pages = {180-191}, year = {2023}, month = feb, abstract = {This article proposes automated methods for threat analysis using a model-based engineering methodology that provides precise guarantees with respect to safety goals. This is accomplished by proposing an intruder model for automotive SOA which together with the system architecture and the loss scenarios identified by safety analysis are used as input for computing assets, impact rating, damage/threat scenarios, and attack paths. To validate the proposed methodology, we developed a faithful model of the autonomous driving functions of the Apollo framework, a widely used open source autonomous driving stack. The proposed machinery automatically enumerates several attack paths on Apollo, including attack paths not reported in the literature.}, isbn = {978-989-758-624-8}, issn = {2184-4356}, doi = {10.5220/0011786400003405}, keywords = {automotive, threat analysis, service-oriented architectures, Apollo, automation, safe and secure-by-design, MbSE, Model-based Systems Engineering, AutoFOCUS3, AF3}, } @inproceedings{, author = {Dantas, Yuri Gil and Munaro, Tiziano and C{\^{a}}rlan, Carmen and Nigam, Vivek and Barner, Simon and Fan, Shiqing and Pretschner, Alexander and Sch{\"{o}}pp, Ulrich and Tverdyshev, Sergey}, title = {A Model-based System Engineering Plugin for Safety Architecture Pattern Synthesis}, booktitle = {Proceeding of the 10th International Conference on Model-Driven Engineering and Software Development (MODELSWARD)}, publisher = {SCITEPRESS}, pages = {36--47}, year = {2022}, month = feb, abstract = {Safety architecture patterns are abstract representations to address faults in the system architecture. In the current state of practice, the decision of which safety architecture pattern to deploy and where in the system architecture is carried out manually by a safety expert. This decision may be time consuming or even lead to human errors. This paper presents Safety Pattern Synthesis, a tool for automating the recommendation of safety architecture patterns during the design of safety-critical systems: 1) Safety Pattern Synthesis recommends patterns to address faults in the system architecture (possibly resulting in more than one architectural solution), 2) the user selects the system architecture with patterns based on, e.g., the criteria provided by Safety Pattern Synthesis, and 3) Safety Pattern Synthesis provides certain requirements that shall be considered in the overall safety engineering process. The proposed tool has been implemented as a plugin in the model-based system engineering tool called AutoFOCUS3. Safety Pattern Synthesis is implemented in Java while using a logic-programming engine as a backend to reason about the safety of the system architecture. This paper provides implementation details about Safety Pattern Synthesis and its applicability in an industrial case study taken from the automotive domain.}, isbn = {978-989-758-550-0}, doi = {10.5220/0010831700003119}, keywords = {Model-based Systems Engineering, MbSE, Safety Architecture Patterns, Automation, Tooling, DSE}, } @inproceedings{VNC 2020, author = {Dantas, Yuri Gil and Nigam, Vivek and Talcott, Carolyn}, title = {A Formal Security Assessment Framework for Cooperative Adaptive Cruise Control}, booktitle = {IEEE Vehicular Networking Conference (VNC)}, publisher = {IEEE}, pages = {1-8}, year = {2020}, month = dec, abstract = {For increased safety and fuel-efficiency, vehicle platoons use Cooperative Adaptive Cruise Control (CACC) where vehicles adapt their state, incl. speed and position, based on information exchanged between vehicles. Intruders, however, may carry out attacks against CACC platoons by exploiting the communication channels used to cause harm, e.g., a vehicle crash. Therefore, during design-phase, engineers should provide evidence supporting platoon security. This paper proposes a formal framework for the security verification of CACC platoons to provide such evidence based on precise mathematical models. Our vehicle platoon models support the specification of both cyber, e.g., communication protocols, and physical, e.g., speeds, position, vehicle behaviors. Moreover, we propose intruder models that are parametric on his capabilities of manipulating communication channels, i.e., message injection and blocking. Our model is implemented enabling the automated formal verification involving both platoon and intruder models. We validate our machinery with a number of attacks taken from the literature and novel attacks discovered by using our formal machinery.}, doi = {10.1109/VNC51378.2020.9318334}, keywords = {attacks, formal verification, platoon, security, AutoFOCUS3, AF3}, } @inproceedings{, author = {Dantas, Yuri Gil and Kondeva, Antoaneta and Nigam, Vivek}, title = {Less Manual Work for Safety Engineers: Towards an Automated Safety Reasoning with Safety Patterns (Application Paper)}, booktitle = {36th International Conference on Logic Programming (ICLP)}, year = {2020}, month = sep, address = {Rende, Italy}, abstract = {The development of safety-critical systems requires the control of hazards that can potentially cause harm. To this end, safety engineers rely during the development phase on architectural solutions, called safety patterns, such as safety monitors, voters, and watchdogs. The goal of these patterns is to control (identified) faults that can trigger hazards. Safety patterns can control such faults by e.g., increasing the redundancy of the system. Currently, the reasoning of which pattern to use at which part of the target system to control which hazard is documented mostly in textual form or by means of models, such as GSN-models, with limited support for automation. This paper proposes the use of logic programming engines for the auto- mated reasoning about system safety. We propose a domain-specific language for embedded system safety and specify as disjunctive logic programs reasoning principles used by safety engineers to deploy safety patterns, e.g., when to use safety monitors, or watchdogs. Our machinery enables two types of automated safety reasoning: (1) identification of which hazards can be controlled and which ones cannot be controlled by the existing safety patterns; and (2) automated recommendation of which patterns could be used at which place of the system to control potential hazards. Finally, we apply our machinery to two examples taken from the automotive domain: an adaptive cruise control system and a battery management system.}, } @inproceedings{, author = {Dantas, Yuri Gil and Kondeva, Antoaneta and Nigam, Vivek}, title = {Towards Automating Safety and Security Co-Analysis with Patterns}, booktitle = {39th International Conference on Computer Safety, Reliability and Security (SafeComp)}, year = {2020}, month = sep, address = {Lisbon, Portugal}, howpublished = {Position paper}, } @proceedings{2019Santosa, author = {Cassimiro T. dos Santos, Aellison and Schneider, Ben and Nigam, Vivek}, title = {TSNSCHED: Automated Schedule Generation for Time Sensitive Networking}, booktitle = {Formal Methods in Computer-Aided Design 2019}, year = {2019}, month = oct, timestamp = 2019.10.23, location = {San Jose, California, USA}, abstract = {Time Sensitive Networking (TSN) is a set of standards enabling high performance deterministic communication using different scheduling mechanisms. Due to the size of industrial networks, configuring TSN networks is challenging to be done manually. We present TSNsched, a tool for automatic generation of schedules for TSN. TSNsched takes as input the logical topology of a network, expressed as flows, and outputs schedules for TSN switches using an SMT-solver. The generated schedule guarantees the desired network performance (specified in terms of latency and jitter), if such schedules exist. TSNsched can synthesize IEEE 802.1Qbv schedules and supports unicast and multicast flows, such as, in Publish/Subscribe networks. TSNsched can be run as a standalone tool and also allows rapid prototyping with the available JAVA API. We evaluate TSNsched on a number of realistic-size network topologies. TSNsched can generate high performance schedules, with average latency less than 1000us, and average jitter less than 20us, for TSN networks, with up to 73 subscribers and up to 10 multicast flows.}, } @inproceedings{alturki19cathy, author = {Alturki, Musab A. and Ban Kirigin, Tajana and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, title = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {11565}, pages = {192--213}, year = {2019}, } @conference{, author = {Alturki, Musab A. and Ban Kirigin, Tajana and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn}, title = {A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, series = {LNCS}, number = {11565}, pages = {192--213}, year = {2019}, doi = {10.1007/978-3-030-19052-1}, } @article{santos19jaihc, author = {Cassimiro T. dos Santos, Aellison and Filho, Jos{\'{e}} L. Soares and Silva, {{$1A}}villa {{$1I}}. S. and Nigam, Vivek and Fonseca, Iguatemi}, title = {BLE Injection-Free Attack: A Novel Attack On Bluetooth LowEnergy Devices}, journal = {Journal of Ambient Intelligence and Humanized Computing}, year = {2019}, } @inproceedings{carlan19wosocer, author = {Nigam, Vivek and Tsalidis, Alexandros and Voss, Sebastian and C{\^{a}}rlan, Carmen}, title = {ExplicitCase: Tool-support for Creating and Maintaining Assurance Arguments Integrated with System Models}, booktitle = {2019 IEEE International Symposium on Software Reliability Engineering Workshops ({ISSREW})}, year = {2019}, abstract = {Assurance cases are collections of standard-mandated documents that entail the specification of system's objectives and a collection of processes, development or verification evidence regarding the satisfaction of the respective objectives. A considerable amount of work has been done in the direction of modelling assurance cases, to support communication and reasoning regarding the system's safety. In this work, we present a set of features of ExplicitCase - a tool for modeling assurance cases. While there is a plethora of tools for creating and managing model-based assurance cases, the uniqueness of our tool is that it integrates assurance case models with system models created in AutoFOCUS3 (AF3) - an open-source model-based development tool for embedded software systems. While trying to keep up with state-of-the-art assurance case editors, the newly implemented features support assurance case creation using typed patterns, change impact analysis for assurance cases, assessment of the confidence in the created assurance arguments, export of the argumentation diagrams generated in ExplicitCase and integration of assurance case models with system models created in AutoFOCUS3. In particular, based on the integration with AF3 system models, we propose automatic support for detecting the impact of a change within system models on the assurance case model, thus enabling the integrated development of system and assurance case models.}, doi = {10.1109/ISSREW.2019.00093}, keywords = {AutoFOCUS3, model-based safety cases, ExplicitCase, Model-based systems engineering, MbSE}, } @inproceedings{nigam19etfa, author = {Nigam, Vivek and Talcott, Carolyn}, title = {Formal Security Verification of Industry 4.0 Applications}, booktitle = {24th {IEEE} International Conference on Emerging Technologies and Factory Automation, {ETFA} 2019, Zaragoza, Spain, September 10-13, 2019}, publisher = {{IEEE}}, pages = {1043--1050}, year = {2019}, doi = {10.1109/ETFA.2019.8869428}, } @article{DBLP:journals/tcs/NigamT19, author = {Nigam, Vivek and Thiemann, Ren{\'{e}}}, title = {Logical and Semantic Frameworks with Applications}, journal = {Theor. Comput. Sci.}, volume = {781}, pages = {1--2}, year = {2019}, doi = {10.1016/j.tcs.2019.05.023}, url = {https://doi.org/10.1016/j.tcs.2019.05.023}, } @inproceedings{kondeva19wosocer, author = {Kondeva, Antoaneta and C{\^{a}}rlan, Carmen and Rue{\ss}, Harald and Nigam, Vivek}, title = {On Computer-Aided Techniques for Supporting Safety and Security Co-Engineering}, booktitle = {Proceedings of the 2019 IEEE International Symposium on Software Reliability Engineering Workshops ({ISSREW})}, publisher = {IEEE}, year = {2019}, abstract = {With the increasing system interconnectivity, cyberattacks on safety-critical systems can lead to catastrophic events. This calls for a better safety and security integration. Indeed, a safety assessment contains security relevant information, such as, key safety hazards, that shall not be triggered by cyber-attacks. Guidelines, such as, SAE J3061 and ED202A, already recommend to exchange information gathered by safety and security engineers during different phases of development. However, these guidelines do not specify exactly how and which information shall be exchanged. We propose a methodology for enabling computer aided techniques for extracting security relevant information from safety analysis. In particular, we propose techniques for automatically constructing Attack Trees from safety artefacts such as fault trees, hazard analysis and safety patterns. Lastly, we illustrate these techniques on an Industry 4.0 application.}, doi = {10.1109/ISSREW.2019.00095}, keywords = {Model-based systems engineering, MbSE}, } @inproceedings{urquiza19csf, author = {Aires Urquiza, Abra{\~{a}}o and Alturki, Musab A. and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre}, title = {Resource-Bounded Intruders in Denial of Service Attacks}, booktitle = {32nd {IEEE} Computer Security Foundations Symposium, {CSF} 2019, Hoboken, NJ, USA, June 25-28, 2019}, publisher = {{IEEE}}, pages = {382--396}, year = {2019}, doi = {10.1109/CSF.2019.00033}, } @article{DBLP:journals/mscs/KanovichKNS19, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {Subexponentials in non-commutative linear logic}, journal = {Mathematical Structures in Computer Science}, volume = {29}, number = {8}, pages = {1217--1249}, year = {2019}, doi = {10.1017/S0960129518000117}, url = {https://doi.org/10.1017/S0960129518000117}, } @inproceedings{nigam19cathy, author = {Nigam, Vivek and Talcott, Carolyn and Aires Urquiza, Abra{\~{a}}o}, title = {Symbolic Timed Trace Equivalence}, booktitle = {Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {11565}, pages = {89--111}, year = {2019}, doi = {10.1007/978-3-030-19052-1\_8}, } @inproceedings{reich19aviose, author = {Reich, Marina and Chuprina, Tatiana and Nigam, Vivek}, title = {Towards Computer-Aided Software Requirements Process}, booktitle = {Proceedings of the Workshops of the Software Engineering Conference 2019, Stuttgart, Germany, February 19, 2019.}, publisher = {{IEEE}}, pages = {75--78}, year = {2019}, } @inproceedings{cassimiro19fmcad, author = {Schneider, Ben and Nigam, Vivek}, title = {TSNsched: Automated Schedule Generation for Time Sensitive Networking}, booktitle = {2019 Formal Methods in Computer Aided Design, {FMCAD} 2019, San Jose, CA, USA, October 22-25, 2019}, pages = {69--77}, year = {2019}, doi = {10.23919/FMCAD.2019.8894249}, } @article{Shankar, author = {Beyene, Tewodros and Herrera, Christian and Nigam, Vivek}, title = {Verification of Ada Programs with AdaHorn}, journal = {Ada User Journal}, volume = {40}, number = {2}, pages = {103-108}, year = {2019}, abstract = {We propose AdaHorn , a model checker for verification of Ada programs with respect to correctness properties given as assertions. AdaHorn translates an Ada program together with its assertion into a set of Constrained Horn Clauses, and feeds it to a Horn constraints solver. We evaluate the performance of AdaHorn on a set of Ada programs inspired by C programs from the software verification competition (SV-COMP). Our experimental results show that AdaHorn outputs correct results in more cases than GNATProve, which is a widely used Ada verification framework.}, } @article{beyene19, author = {Nigam, Vivek}, title = {Verification of Ada Programs with AdaHorn}, booktitle = {The 9th IEEE International Workshop on Software Certification {WoSoCer}}, journal = {Ada User Journal}, year = {2019}, } @inproceedings{kanovich18ijcar, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {A Logical Framework with Commutative and Non-commutative Subexponentials}, booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings}, pages = {228--245}, year = {2018}, abstract = {Logical frameworks allow the specification of deductive systems usingthe same logical machinery. Linear logical frameworks have been successfullyused for the specification of a number of computational, logics and proofsystems. Its success relies on the fact that formulas can be distinguished as linear,which behave intuitively as resources, and unbounded, which behave intuitionistically.Commutative subexponentials enhance the expressiveness of linear logicframeworks by allowing the distinction of multiple contexts. These contexts maybehave as multisets of formulas or sets of formulas. Motivated by applicationsin distributed systems and in type-logical grammar, we propose a linear logicalframework containing both commutative and non-commutative subexponentials.Non-commutative subexponentials can be used to specify contexts which behaveas lists, not multisets, of formulas. In addition, motivated by our applications intype-logical grammar, where the weakenening rule is disallowed, we investigatethe proof theory of formulas that can only contract, but not weaken. In fact, ourcontraction is non-local. We demonstrate that under some conditions such formulasmay be treated as unbounded formulas, which behave intuitionistically.}, doi = {10.1007/978-3-319-94205-6\_16}, url = {https://doi.org/10.1007/978-3-319-94205-6\_16}, } @article{benton18scp, author = {Benton, Nick and Hofmann, Martin and Nigam, Vivek}, title = {Effect-dependent transformations for concurrent programs}, journal = {Sci. Comput. Program.}, volume = {155}, pages = {27--51}, year = {2018}, abstract = {We describe a denotational semantics for an abstract effect system for a higher-order,shared-variable concurrent programming language. We prove the soundness of a numberof general effect-based program equivalences, including a parallelization equationthat specifies sufficient conditions for replacing sequential composition with parallelcomposition. Effect annotations are relative to abstract locations specified by contractsrather than physical footprints allowing us in particular to show the soundness of sometransformations involving fine-grained concurrent data structures, such as MichaelScottqueues, that allow concurrent access to different parts of mutable data structures.Our semantics is based on refining a trace-based semantics for first-order programsdue to Brookes. By moving from concrete to abstract locations, and adding type refinementsthat capture the possible side-effects of both expressions and their concurrentenvironments, we are able to validate many equivalences that do not hold in an unrefinedmodel. The meanings of types are expressed using a game-based logical relationover sets of traces. Two programs e1 and e2 are logically related if one is able to solvea two-player game: for any trace with result value v1 in the semantics of e1 (challenge)that the player presents, the opponent can present an (response) equivalent trace in thesemantics of e2 with a logically related result value v2.}, doi = {10.1016/j.scico.2017.11.001}, url = {https://doi.org/10.1016/j.scico.2017.11.001}, } @inproceedings{chen18ifipsec, author = {Chen, Wei and Lin, Yuhui and Galpin, Vashti and Nigam, Vivek and Lee, Myungjin and Aspinall, David}, title = {Formal Analysis of Sneak-Peek: A Data Centre Attack and its Mitigations}, booktitle = { 33rd IFIP TC-11 SEC 2018 International Conference on Information Security and Privacy Protection ({IFIPSEC 2018}) - Poznan, Poland}, year = {2018}, abstract = {Attackers can exploit covert channels, such as timing side-channels, totransmit information without data owners or network administrators being aware.Sneak-Peek is a recently considered data centre attack, where, in a multi-tenantsetting, an insider attacker can communicate with colluding outsiders by intentionallyadding delays to traffic on logically isolated but physically shared links.Timing attack mitigations typically introduce delays or randomness which canmake it difficult to understand the trade-off between level of security (bandwidthof the covert channel) and performance loss. We demonstrate that formal methodscan help. We analyse the impacts of two Sneak-Peek mitigations, namely,noise addition and path hopping. We provide a precise mathematical model ofthe attack and of the effectiveness these defences. This mathematical analysis isextended by two tool-based stochastic formal models, one formalized in UPPAALand the other in CARMA. The formal models can capture more general and largernetworks than a paper-based analysis, can be used to check properties and makemeasurements, and are more easily modifiable than conventional network simulations.With UPPAAL, we can analyse the effectiveness of mitigations and withCARMA, we can analyse how these mitigations affect latencies in typical datacentre topologies. As results, we show that using a selective strategy for path hoppingis better than a random strategy, that using the two defences in conjunctionmay actually be worse than using a single defence, and we show the connectionbetween hop frequency and network latency.}, } @article{DBLP:journals/jlp/LemosDFN18, author = {Lemos, Marcilio and Dantas, Yuri Gil and Fonseca, Iguatemi and Nigam, Vivek}, title = {On the accuracy of formal verification of selective defenses for TDoS attacks}, journal = {J. Log. Algebr. Meth. Program.}, volume = {94}, pages = {45--67}, year = {2018}, abstract = {Telephony Denial of Service (TDoS) attacks target telephony services, such as Voice over IP (VoIP), not allowing legitimate users to make calls. There are few defenses that attempt to mitigate TDoS attacks, most of them using IP filtering, with limited applicability. In our previous work, we proposed to use selective strategies for mitigating HTTP Application-Layer DDoS Attacks demonstrating their effectiveness in mitigating different types of attacks. Developing such types of defenses is challenging as there are many design options, e.g., which dropping functions and selection algorithms to use. Our first contribution is to demonstrate both experimentally and by using formal verification that selective strategies are suitable for mitigating TDoS attacks. We used our formal model to help decide which selective strategies to use with much less effort than carrying out experiments. Our second contribution is a detailed comparison of the results obtained from our formal models and the results obtained by carrying out experiments. We demonstrate that formal methods is a powerful tool for specifying defenses for mitigating Distributed Denial of Service attacks allowing to increase our confidence on the proposed defense before actual implementation.}, doi = {10.1016/j.jlamp.2017.09.001}, url = {https://doi.org/10.1016/j.jlamp.2017.09.001}, } @article{benton18lmcs, author = {Benton, Nick and Hofmann, Martin and Nigam, Vivek}, title = {Proof-Relevant Logical Relations for Name Generation}, journal = {Accepted to Logical Methods in Computer Science}, year = {2018}, abstract = {Pitts and Stark’s v-calculus is a paradigmatic total language for studying the problem ofcontextual equivalence in higher-order languages with name generation. Models for the ν-calculusthat validate basic equivalences concerning names may be constructed using functor categories ornominal sets, with a dynamic allocation monad used to model computations that may allocate freshnames. If recursion is added to the language and one attempts to adapt the models from (nominal)sets to (nominal) domains, however, the direct-style construction of the allocation monad no longerworks. This issue has previously been addressed by using a monad that combines dynamic allocationwith continuations, at some cost to abstraction.This paper presents a direct-style model of a v-calculus-like language with recursion using thenovel framework of proof-relevant logical relations, in which logical relations also contain objects(or proofs) demonstrating the equivalence of (the semantic counterparts of) programs. Apart fromproviding a fresh solution to an old problem, this work provides an accessible setting in which tointroduce the use of proof-relevant logical relations, free of the additional complexities associatedwith their use for more sophisticated languages.}, } @inproceedings{kanovich18fcs, author = {Alturki, Musab A. and Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Ban Kirigin, Tajana}, title = {Statistical Model Checking of Guessing and Timing Attacks on Distance-bounding Protocols.}, booktitle = {"Workshop on Foundations of Computer Security"}, year = {2018}, abstract = {Distance-bounding (DB) protocols were proposed tothwart relay attacks on proximity-based access control systems.In a DB protocol, the verifier computes an upper bound on thedistance to the prover by measuring the time needed for a signalto travel to the prover and back. DB protocols are, however,vulnerable to distance fraud, in which a dishonest prover isable to manipulate the distance bound computed by an honestverifier. Despite their conceptual simplicity, devising a formalcharacterization of DB protocols and distance fraud attacks thatis amenable to automated formal analysis is non-trivial, primarilybecause of their real-time and probabilistic nature. In this work,we present a framework, based on rewriting logic, for formallyanalyzing different forms of distance-fraud, including recentlyidentified timing attacks. We introduce a generic, real-time andprobabilistic model of DB protocols and use it to (mechanically)verify false-acceptance and false-rejection probabilities undervarious settings and attacker models through statistical modelchecking with MAUDE and PVESTA. Using this framework,we first accurately confirm known results and then define andquantitatively evaluate new guessing-ahead attack strategies thatwould otherwise be difficult to analyze manually.}, } @article{kanovich18mscs, author = {Kanovich, Max and Kuznetsov, Stepan and Nigam, Vivek and Scedrov, Andre}, title = {Subexponentials in non-commutative linear logic}, journal = {Mathematical Structures in Computer Science}, year = {2018}, abstract = {Linear logical frameworks with subexponentials have been used for the specification of,among other systems, proof systems, concurrent programming languages and linearauthorisation logics. In these frameworks, subexponentials can be configured to allow or notfor the application of the contraction and weakening rules while the exchange rule canalways be applied. This means that formulae in such frameworks can only be organised assets and multisets of formulae not being possible to organise formulae as lists of formulae.This paper investigates the proof theory of linear logic proof systems in thenon-commutative variant. These systems can disallow the application of exchange rule onsome subexponentials. We investigate conditions for when cut elimination is admissible inthe presence of non-commutative subexponentials, investigating the interaction of theexchange rule with the local and non-local contraction rules. We also obtain some newundecidability and decidability results on non-commutative linear logic with subexponentials.}, doi = {10.1017/S0960129518000117}, url = {https://doi.org/10.1017/S0960129518000117}, } @inproceedings{mason17cosim, author = {Mason, Ian and Nigam, Vivek and Talcott, Carolyn and Vasconcelos De Brito, Alisson}, title = {A Framework for Analyzing Adaptive Autonomous Aerial Vehicles}, booktitle = {Software Engineering and Formal Methods - {SEFM} 2017 Collocated Workshops: DataMod, FAACS, MSE, CoSim-CPS, and FOCLASA, Trento, Italy, September 4-5, 2017, Revised Selected Papers}, pages = {406--422}, year = {2017}, abstract = {Unmanned aerial vehicles (UAVs), a.k.a. drones, are becoming increasingly popular due to great advancements in their control mechanisms and price reduction. UAVs are being used in applications such as package delivery, plantation and railroad track monitoring, where UAVs carry out tasks in an automated fashion. Devising how UAVs achieve a task is challenging as the environment where UAVs are deployed is normally unpredictable, for example, due to winds. Formal methods can help engineers to specify flight strategies and to evaluate how well UAVs are going to perform to achieve a task. This paper proposes a formal framework where engineers can raise the confidence in their UAV specification by using symbolic, simulation and statistical and model checking methods. Our framework is constructed over three main components: the behavior of UAVs and the environment are specified in a formal executable language; the UAV's physical model is specified by a simulator; and statistical model checking algorithms are used for the analysis of system behaviors. We demonstrate the effectiveness of our framework by means of several scenarios involving multiple drones.}, doi = {10.1007/978-3-319-74781-1_28}, url = {https://doi.org/10.1007/978-3-319-74781-1_28}, } @article{DBLP:journals/mscs/KanovichKNSTP17, author = {Kanovich, Max and Ban Kirigin, Tajana and Nigam, Vivek and Scedrov, Andre and Perovic, Ranko and Talcott, Carolyn}, editor = {Kr{\"{o}}ger, Torsten and Wahl, Friedrich M.}, title = {A rewriting framework and logic for activities subject to regulations}, journal = {Mathematical Structures in Computer Science}, volume = {27}, number = {3}, pages = {332--375}, year = {2017}, abstract = {Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.}, doi = {10.1017/S096012951500016X}, url = {https://doi.org/10.1017/S096012951500016X}, } @article{DBLP:journals/dafes/BarrosONB17, author = {Barros, Jose de Sousa and Oliveira, Thyago and Nigam, Vivek and Brito, Alisson}, title = {Analysis of design strategies for unmanned aerial vehicles using co-simulation}, journal = {Design Autom. for Emb. Sys.}, volume = {21}, number = {3-4}, pages = {157--172}, year = {2017}, abstract = {Designing critical embedded systems, like UAVs is not a trivial task because it brings the challenge of dealing with the uncertainty that is inherent to this type of systems, e.g., winds, GPS uncertainty, etc. Simulation and verification tools that provide a level of confidence can help design such systems and increase the safety of specified cyber-physical systems before deployment. This paper presents a framework for evaluating flight strategies of UAVs. Our framework is constructed by integrating, using high-level architecture, Ptolemy, a high level specification tool, and SITL/Ardupilot, a domain specific UAV simulator. It allows to evaluate flight strategies under the presence of uncertainty, such as winds, with a level of confidence by constructing a sufficiently large number of simulations. Its effectiveness is demonstrated by testing two different flight strategies in two scenarios under different wind intensities. We measure the flight quality providing quantitative information about the quality of the tested flight strategy, such as distance traveled, with a confidence of 95% and error of 8%.}, doi = {10.1007/s10617-017-9190-z}, url = {https://doi.org/10.1007/s10617-017-9190-z}, } @article{DBLP:journals/tcs/NigamOP17, author = {Nigam, Vivek and Olarte, Carlos and Pimentel, Elaine}, title = {On subexponentials, focusing and modalities in concurrent systems}, journal = {Theor. Comput. Sci.}, volume = {693}, pages = {35--58}, year = {2017}, abstract = {In this work we present the focused proof system SELLF⋒, which extends intuitionistic linear logic with subexponentials with the ability of quantifying over them, hence allowing for the use of an arbitrary number of modalities. We show that the view of subexponentials as specific modalities is general enough to give a modular encoding of different flavors of Concurrent Constraint Programming (CCP), a simple and powerful model of concurrency. More precisely, we encode CCP calculi capturing time, spatial and epistemic behaviors into SELLF⋒, thus providing a proof theoretic foundation for those calculi and, at the same time, setting SELLF⋒ as a general framework for specifying such systems.}, doi = {10.1016/j.tcs.2017.06.009}, url = {https://doi.org/10.1016/j.tcs.2017.06.009}, } @inproceedings{DBLP:conf/sec/PascoalDFN17, author = {Pascoal, Tulio and Dantas, Yuri Gil and Fonseca, Iguatemi and Nigam, Vivek}, title = {Slow {TCAM} Exhaustion DDoS Attack}, booktitle = {{ICT} Systems Security and Privacy Protection - 32nd {IFIP} {TC} 11 International Conference, {SEC} 2017, Rome, Italy, May 29-31, 2017, Proceedings}, pages = {17--31}, year = {2017}, abstract = {Software Defined Networks (SDN) facilitate network management by decoupling the data plane which forwards packets using efficient switches from the control plane by leaving the decisions on how packets should be forwarded to a (centralized) controller. However, due to limitations on the number of forwarding rules a switch can store in its TCAM memory, SDN networks have been subject to saturation and TCAM exhaustion attacks where the attacker is able to deny service by forcing a target switch to install a great number of rules. An underlying assumption is that these attacks are carried out by sending a high rate of unique packets. This paper shows that this assumption is not necessarily true and that SDNs are vulnerable to Slow TCAM exhaustion attacks (Slow-TCAM). We analyse this attack arguing that existing defenses for saturation and TCAM exhaustion attacks are not able to mitigate Slow-TCAM due to its relatively low traffic rate. We then propose a novel defense called SIFT based on selective strategies demonstrating its effectiveness against the Slow-TCAM attack.}, doi = {10.1007/978-3-319-58469-0_2}, url = {https://doi.org/10.1007/978-3-319-58469-0_2}, } @article{DBLP:journals/jcs/KanovichKNST17, author = {Kanovich, Max and Nigam, Vivek and Scedrov, Andre and Talcott, Carolyn and Ban Kirigin, Tajana}, title = {Time, computational complexity, and probability in the analysis of distance-bounding protocols}, journal = {Journal of Computer Security}, volume = {25}, number = {6}, pages = {585--630}, year = {2017}, abstract = {Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with an attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.}, doi = {10.3233/JCS-0560}, url = {https://doi.org/10.3233/JCS-0560}, }