Visible to the public Biblio

Filters: Keyword is formal verification  [Clear All Filters]
2019
Protzenko, Jonathan, Beurdouche, Benjamin, Merigoux, Denis, Bhargavan, Karthikeyan.  2019.  Formally Verified Cryptographic Web Applications in WebAssembly. 2019 IEEE Symposium on Security and Privacy (SP). :1256–1274.
After suffering decades of high-profile attacks, the need for formal verification of security-critical software has never been clearer. Verification-oriented programming languages like F* are now being used to build high-assurance cryptographic libraries and implementations of standard protocols like TLS. In this paper, we seek to apply these verification techniques to modern Web applications, like WhatsApp, that embed sophisticated custom cryptographic components. The problem is that these components are often implemented in JavaScript, a language that is both hostile to cryptographic code and hard to reason about. So we instead target WebAssembly, a new instruction set that is supported by all major JavaScript runtimes. We present a new toolchain that compiles Low*, a low-level subset of the F* programming language, into WebAssembly. Unlike other WebAssembly compilers like Emscripten, our compilation pipeline is focused on compactness and auditability: we formalize the full translation rules in the paper and implement it in a few thousand lines of OCaml. Using this toolchain, we present two case studies. First, we build WHACL*, a WebAssembly version of the existing, verified HACL* cryptographic library. Then, we present LibSignal*, a brand new, verified implementation of the Signal protocol in WebAssembly, that can be readily used by messaging applications like WhatsApp, Skype, and Signal.
Elfar, Mahmoud, Zhu, Haibei, Cummings, M. L., Pajic, Miroslav.  2019.  Security-Aware Synthesis of Human-UAV Protocols. 2019 International Conference on Robotics and Automation (ICRA). :8011–8017.
In this work, we synthesize collaboration protocols for human-unmanned aerial vehicle (H-UAV) command and control systems, where the human operator aids in securing the UAV by intermittently performing geolocation tasks to confirm its reported location. We first present a stochastic game-based model for the system that accounts for both the operator and an adversary capable of launching stealthy false-data injection attacks, causing the UAV to deviate from its path. We also describe a synthesis challenge due to the UAV's hidden-information constraint. Next, we perform human experiments using a developed RESCHU-SA testbed to recognize the geolocation strategies that operators adopt. Furthermore, we deploy machine learning techniques on the collected experimental data to predict the correctness of a geolocation task at a given location based on its geographical features. By representing the model as a delayed-action game and formalizing the system objectives, we utilize off-the-shelf model checkers to synthesize protocols for the human-UAV coalition that satisfy these objectives. Finally, we demonstrate the usefulness of the H-UAV protocol synthesis through a case study where the protocols are experimentally analyzed and further evaluated by human operators.
Mahale, Anusha, B.S., Kariyappa.  2019.  Architecture Analysis and Verification of I3C Protocol. 2019 3rd International Conference on Electronics, Communication and Aerospace Technology (ICECA). :930-935.

In VLSI industry the design cycle is categorized into Front End Design and Back End Design. Front End Design flow is from Specifications to functional verification of RTL design. Back End Design is from logic synthesis to fabrication of chip. Handheld devices like Mobile SOC's is an amalgamation of many components like GPU, camera, sensor, display etc. on one single chip. In order to integrate these components protocols are needed. One such protocol in the emerging trend is I3C protocol. I3C is abbreviated as Improved Inter Integrated Circuit developed by Mobile Industry Processor Interface (MIPI) alliance. Most probably used for the interconnection of sensors in Mobile SOC's. The main motivation of adapting the standard is for the increase speed and low pin count in most of the hardware chips. The bus protocol is backward compatible with I2C devices. The paper includes detailed study I3C bus protocol and developing verification environment for the protocol. The test bench environment is written and verified using system Verilog and UVM. The Universal Verification Methodology (UVM) is base class library built using System Verilog which provides the fundamental blocks needed to quickly develop reusable and well-constructed verification components and test environments. The Functional Coverage of around 93.55 % and Code Coverage of around 98.89 % is achieved by verification closure.

Hu, Yayun, Li, Dongfang.  2019.  Formal Verification Technology for Asynchronous Communication Protocol. 2019 IEEE 19th International Conference on Software Quality, Reliability and Security Companion (QRS-C). :482-486.

For aerospace FPGA software products, traditional simulation method faces severe challenges to verify product requirements under complicated scenarios. Given the increasing maturity of formal verification technology, this method can significantly improve verification work efficiency and product design quality, by expanding coverage on those "blind spots" in product design which were not easily identified previously. Taking UART communication as an example, this paper proposes several critical points to use formal verification for asynchronous communication protocol. Experiments and practices indicate that formal verification for asynchronous communication protocol can effectively reduce the time required, ensure a complete verification process and more importantly, achieve more accurate and intuitive results.

Canetti, Ran, Stoughton, Alley, Varia, Mayank.  2019.  EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :167–16716.
We present a methodology for using the EasyCrypt proof assistant (originally designed for mechanizing the generation of proofs of game-based security of cryptographic schemes and protocols) to mechanize proofs of security of cryptographic protocols within the universally composable (UC) security framework. This allows, for the first time, the mechanization and formal verification of the entire sequence of steps needed for proving simulation-based security in a modular way: Specifying a protocol and the desired ideal functionality; Constructing a simulator and demonstrating its validity, via reduction to hard computational problems; Invoking the universal composition operation and demonstrating that it indeed preserves security. We demonstrate our methodology on a simple example: stating and proving the security of secure message communication via a one-time pad, where the key comes from a Diffie-Hellman key-exchange, assuming ideally authenticated communication. We first put together EasyCrypt-verified proofs that: (a) the Diffie-Hellman protocol UC-realizes an ideal key-exchange functionality, assuming hardness of the Decisional Diffie-Hellman problem, and (b) one-time-pad encryption, with a key obtained using ideal key-exchange, UC-realizes an ideal secure-communication functionality. We then mechanically combine the two proofs into an EasyCrypt-verified proof that the composed protocol realizes the same ideal secure-communication functionality. Although formulating a methodology that is both sound and workable has proven to be a complex task, we are hopeful that it will prove to be the basis for mechanized UC security analyses for significantly more complex protocols and tasks.
2018
Dewoprabowo, Ridhwan, Arzaki, Muhammad, Rusmawati, Yanti.  2018.  Formal Verification of Divide and Conquer Key Distribution Protocol Using ProVerif and TLA+. 2018 International Conference on Advanced Computer Science and Information Systems (ICACSIS). :451-458.

We conduct formal verification of the divide and conquer key distribution scheme (DC DHKE)-a contributory group key agreement that uses a quasilinear amount of exponentiations with respect to the number of communicating parties. The verification is conducted using both ProVerif and TLA+ as tools. ProVerif is used to verify the protocol correctness as well as its security against passive attacker; while TLA+ is utilized to verify whether all participants in the protocol retrieve the mutual key simultaneously. We also verify the ING and GDH.3 protocol for comparative purposes. The verification results show that the ING, GDH.3, and DC DHKE protocols satisfy the pre-meditated correctness, security, and liveness properties. However, the GDH.3 protocol does not satisfy the liveness property stating that all participants obtain the mutual key at the same time.

Harrison, William L., Allwein, Gerard.  2018.  Semantics-Directed Prototyping of Hardware Runtime Monitors. 2018 International Symposium on Rapid System Prototyping (RSP). :42-48.

Building memory protection mechanisms into embedded hardware is attractive because it has the potential to neutralize a host of software-based attacks with relatively small performance overhead. A hardware monitor, being at the lowest level of the system stack, is more difficult to bypass than a software monitor and hardware-based protections are also potentially more fine-grained than is possible in software: an individual instruction executing on a processor may entail multiple memory accesses, all of which may be tracked in hardware. Finally, hardware-based protection can be performed without the necessity of altering application binaries. This article presents a proof-of-concept codesign of a small embedded processor with a hardware monitor protecting against ROP-style code reuse attacks. While the case study is small, it indicates, we argue, an approach to rapid-prototyping runtime monitors in hardware that is quick, flexible, and extensible as well as being amenable to formal verification.

Dreier, Jannik, Hirschi, Lucca, Radomirovic, Sasa, Sasse, Ralf.  2018.  Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. 2018 IEEE 31st Computer Security Foundations Symposium (CSF). :359-373.

Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. The Tamarin prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes Tamarin the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.

Nichols, W., Hawrylak, P. J., Hale, J., Papa, M..  2018.  Methodology to Estimate Attack Graph System State from a Simulation of a Nuclear Research Reactor. 2018 Resilience Week (RWS). :84-87.
Hybrid attack graphs are a powerful tool when analyzing the cybersecurity of a cyber-physical system. However, it is important to ensure that this tool correctly models reality, particularly when modelling safety-critical applications, such as a nuclear reactor. By automatically verifying that a simulation reaches the state predicted by an attack graph by analyzing the final state of the simulation, this verification procedure can be accomplished. As such, a mechanism to estimate if a simulation reaches the expected state in a hybrid attack graph is proposed here for the nuclear reactor domain.
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.

Neal, T., Sundararajan, K., Woodard, D..  2018.  Exploiting Linguistic Style as a Cognitive Biometric for Continuous Verification. 2018 International Conference on Biometrics (ICB). :270-276.

This paper presents an assessment of continuous verification using linguistic style as a cognitive biometric. In stylometry, it is widely known that linguistic style is highly characteristic of authorship using representations that capture authorial style at character, lexical, syntactic, and semantic levels. In this work, we provide a contrast to previous efforts by implementing a one-class classification problem using Isolation Forests. Our approach demonstrates the usefulness of this classifier for accurately verifying the genuine user, and yields recognition accuracy exceeding 98% using very small training samples of 50 and 100-character blocks.

Duan, Zhangbo, Mao, Hongliang, Chen, Zhidong, Bai, Xiaomin, Hu, Kai, Talpin, Jean-Pierre.  2018.  Formal Modeling and Verification of Blockchain System. Proceedings of the 10th International Conference on Computer Modeling and Simulation. :231-235.

As a decentralized and distributed secure storage technology, the notion of blockchain is now widely used for electronic trading in finance, for issuing digital certificates, for copyrights management, and for many other security-critical applications. With applications in so many domains with high-assurance requirements, the formalization and verification of safety and security properties of blockchain becomes essential, and the aim of the present paper. We present the model-based formalization, simulation and verification of a blockchain protocol by using the SDL formalism of Telelogic Tau. We consider the hierarchical and modular SDL model of the blockchain protocol and exercise a methodology to formally simulate and verify it. This way, we show how to effectively increase the security and safety of blockchain in order to meet high assurance requirements demanded by its application domains. Our work also provides effective support for assessing different network consensus algorithms, which are key components in blockchain protocols, as well as on the topology of blockchain networks. In conclusion, our approach contributes to setting up a verification methodology for future blockchain standards in digital trading.

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.

Kulik, T., Tran-Jørgensen, P. W. V., Boudjadar, J., Schultz, C..  2018.  A Framework for Threat-Driven Cyber Security Verification of IoT Systems. 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). :89-97.

Industrial control systems are changing from monolithic to distributed and interconnected architectures, entering the era of industrial IoT. One fundamental issue is that security properties of such distributed control systems are typically only verified empirically, during development and after system deployment. We propose a novel modelling framework for the security verification of distributed industrial control systems, with the goal of moving towards early design stage formal verification. In our framework we model industrial IoT infrastructures, attack patterns, and mitigation strategies for countering attacks. We conduct model checking-based formal analysis of system security through scenario execution, where the analysed system is exposed to attacks and implement mitigation strategies. We study the applicability of our framework for large systems using a scalability analysis.

Hu, W., Ardeshiricham, A., Gobulukoglu, M. S., Wang, X., Kastner, R..  2018.  Property Specific Information Flow Analysis for Hardware Security Verification. 2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). :1-8.

Hardware information flow analysis detects security vulnerabilities resulting from unintended design flaws, timing channels, and hardware Trojans. These information flow models are typically generated in a general way, which includes a significant amount of redundancy that is irrelevant to the specified security properties. In this work, we propose a property specific approach for information flow security. We create information flow models tailored to the properties to be verified by performing a property specific search to identify security critical paths. This helps find suspicious signals that require closer inspection and quickly eliminates portions of the design that are free of security violations. Our property specific trimming technique reduces the complexity of the security model; this accelerates security verification and restricts potential security violations to a smaller region which helps quickly pinpoint hardware security vulnerabilities.

Luo, Qiming, Lv, Ang, Hou, Ligang, Wang, Zhongchao.  2018.  Realization of System Verification Platform of IoT Smart Node Chip. 2018 IEEE 3rd International Conference on Integrated Circuits and Microsystems (ICICM). :341-344.

With the development of large scale integrated circuits, the functions of the IoT chips have been increasingly perfect. The verification work has become one of the most important aspects. On the one hand, an efficient verification platform can ensure the correctness of the design. On the other hand, it can shorten the chip design cycle and reduce the design cost. In this paper, based on a transmission protocol of the IoT node, we propose a verification method which combines simulation verification and FPGA-based prototype verification. We also constructed a system verification platform for the IoT smart node chip combining two kinds of verification above. We have simulated and verificatied the related functions of the node chip using this platform successfully. It has a great reference value.

Plasencia-Balabarca, F., Mitacc-Meza, E., Raffo-Jara, M., Silva-Cárdenas, C..  2018.  Robust Functional Verification Framework Based in UVM Applied to an AES Encryption Module. 2018 New Generation of CAS (NGCAS). :194-197.

This Since the past century, the digital design industry has performed an outstanding role in the development of electronics. Hence, a great variety of designs are developed daily, these designs must be submitted to high standards of verification in order to ensure the 100% of reliability and the achievement of all design requirements. The Universal Verification Methodology (UVM) is the current standard at the industry for the verification process due to its reusability, scalability, time-efficiency and feasibility of handling high-level designs. This research proposes a functional verification framework using UVM for an AES encryption module based on a very detailed and robust verification plan. This document describes the complete verification process as done in the industry for a popular module used in information-security applications in the field of cryptography, defining the basis for future projects. The overall results show the achievement of the high verification standards required in industry applications and highlight the advantages of UVM against System Verilog-based functional verification and direct verification methodologies previously developed for the AES module.

Deb Nath, Atul Prasad, Bhunia, Swarup, Ray, Sandip.  2018.  ArtiFact: Architecture and CAD Flow for Efficient Formal Verification of SoC Security Policies. 2018 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). :411–416.
Verification of security policies represents one of the most critical, complex, and expensive steps of modern SoC design validation. SoC security policies are typically implemented as part of functional design flow, with a diverse set of protection mechanisms sprinkled across various IP blocks. An obvious upshot is that their verification requires comprehension and analysis of the entire system, representing a scalability bottleneck for verification tools. The scale and complexity of industrial SoC is far beyond the analysis capacity of state-of-the-art formal tools; even simulation-based security verification is severely limited in effectiveness because of the need to exercise subtle corner-cases across the entire system. We address this challenge by developing a novel security architecture that accounts for verification needs from the ground up. Our framework, ArtiFact, provides an alternative architecture for security policy implementation that exploits a flexible, centralized, infrastructure IP and enables scalable, streamlined verification of these policies. With our architecture, verification of system-level security policies reduces to analysis of this single IP and its interfaces, enabling off-the-shelf formal tools to successfully verify these policies. We introduce a CAD flow that supports both formal and dynamic (simulation-based) verification, and is built on top of such off-the-shelf tools. Our approach reduces verification time by over 62X and bug detection time by 34X for illustrative policies.
Khelf, Roumaissa, Ghoualmi-Zine, Nacira.  2018.  IPsec/Firewall Security Policy Analysis: A Survey. 2018 International Conference on Signal, Image, Vision and their Applications (SIVA). :1–7.
As the technology reliance increases, computer networks are getting bigger and larger and so are threats and attacks. Therefore Network security becomes a major concern during this last decade. Network Security requires a combination of hardware devices and software applications. Namely, Firewalls and IPsec gateways are two technologies that provide network security protection and repose on security policies which are maintained to ensure traffic control and network safety. Nevertheless, security policy misconfigurations and inconsistency between the policy's rules produce errors and conflicts, which are often very hard to detect and consequently cause security holes and compromise the entire system functionality. In This paper, we review the related approaches which have been proposed for security policy management along with surveying the literature for conflicts detection and resolution techniques. This work highlights the advantages and limitations of the proposed solutions for security policy verification in IPsec and Firewalls and gives an overall comparison and classification of the existing approaches.
Martiny, Karsten, Elenius, Daniel, Denker, Grit.  2018.  Protecting Privacy with a Declarative Policy Framework. 2018 IEEE 12th International Conference on Semantic Computing (ICSC). :227–234.
This article describes a privacy policy framework that can represent and reason about complex privacy policies. By using a Common Data Model together with a formal shareability theory, this framework enables the specification of expressive policies in a concise way without burdening the user with technical details of the underlying formalism. We also build a privacy policy decision engine that implements the framework and that has been deployed as the policy decision point in a novel enterprise privacy prototype system. Our policy decision engine supports two main uses: (1) interfacing with user interfaces for the creation, validation, and management of privacy policies; and (2) interfacing with systems that manage data requests and replies by coordinating privacy policy engine decisions and access to (encrypted) databases using various privacy enhancing technologies.
2017
Matsuo, S..  2017.  How formal analysis and verification add security to blockchain-based systems. 2017 Formal Methods in Computer Aided Design (FMCAD). :1–4.

Blockchain is an integrated technology to ensure keeping record and process transactions with decentralized manner. It is thought as the foundation of future decentralized ecosystem, and collects much attention. However, the maturity of this technology including security of the fundamental protocol and its applications is not enough, thus we need more research on the security evaluation and verification of Blockchain technology This tutorial explains the current status of the security of this technology, its security layers and possibility of application of formal analysis and verification.

Garcia, R., Modesti, P..  2017.  An IDE for the Design, Verification and Implementation of Security Protocols. 2017 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). :157–163.

Security protocols are critical components for the construction of secure and dependable distributed applications, but their implementation is challenging and error prone. Therefore, tools for formal modelling and analysis of security protocols can be potentially very useful to support software engineers. However, despite such tools have been available for a long time, their adoption outside the research community has been very limited. In fact, most practitioners find such applications too complex and hardly usable for their daily work. In this paper, we present an Integrated Development Environment for the design, verification and implementation of security protocols, aimed at lowering the adoption barrier of formal methods tools for security. In the spirit of Model Driven Development, the environment supports the user in the specification of the model using the simple and intuitive language AnB (and its extension AnBx). Moreover, it provides a push-button solution for the formal verification of the abstract and concrete models, and for the automatic generation of Java implementation. This Eclipse-based IDE leverages on existing languages and tools for modelling and verification of security protocols, such as the AnBx Compiler and Code Generator, the model checker OFMC and the protocol verifier ProVerif.

Madhusudhanan, S., Mallissery, S..  2017.  Provable security analysis of complex or smart computer systems in the smart grid. 2017 IEEE International Conference on Smart Grid and Smart Cities (ICSGSC). :210–214.

Security is an important requirement of every reactive system of the smart gird. The devices connected to the smart system in smart grid are exhaustively used to provide digital information to outside world. The security of such a system is an essential requirement. The most important component of such smart systems is Operating System (OS). This paper mainly focuses on the security of OS by incorporating Access Control Mechanism (ACM) which will improve the efficiency of the smart system. The formal methods use applied mathematics for modelling and analysing of smart systems. In the proposed work Formal Security Analysis (FSA) is used with model checking and hence it helped to prove the security of smart systems. When an Operating System (OS) takes into consideration, it never comes to a halt state. In the proposed work a Transition System (TS) is designed and the desired rules of security are provided by using Linear Temporal Logics (LTL). Unlike other propositional and predicate logic, LTL can model reactive systems with a prediction for the future state of the systems. In the proposed work, Simple Promela Interpreter (SPIN) is used as a model checker that takes LTL and TS of the system as input. Hence it is possible to derive the Büchi automaton from LTL logics and that provides traces of both successful and erroneous computations. Comparison of Büchi automaton with the transition behaviour of the OS will provide the details of security violation in the system. Validation of automaton operations on infinite computational sequences verify that whether systems are provably secure or not. Hence the proposed formal security analysis will provably ensures the security of smart systems in the area of smart grid applications.

Sugumar, G., Mathur, A..  2017.  Testing the Effectiveness of Attack Detection Mechanisms in Industrial Control Systems. 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :138–145.

Industrial Control Systems (ICS) are found in critical infrastructure such as for power generation and water treatment. When security requirements are incorporated into an ICS, one needs to test the additional code and devices added do improve the prevention and detection of cyber attacks. Conducting such tests in legacy systems is a challenge due to the high availability requirement. An approach using Timed Automata (TA) is proposed to overcome this challenge. This approach enables assessment of the effectiveness of an attack detection method based on process invariants. The approach has been demonstrated in a case study on one stage of a 6- stage operational water treatment plant. The model constructed captured the interactions among components in the selected stage. In addition, a set of attacks, attack detection mechanisms, and security specifications were also modeled using TA. These TA models were conjoined into a network and implemented in UPPAAL. The models so implemented were found effective in detecting the attacks considered. The study suggests the use of TA as an effective tool to model an ICS and study its attack detection mechanisms as a complement to doing so in a real plant-operational or under design.

Kang, E. Y., Mu, D., Huang, L., Lan, Q..  2017.  Verification and Validation of a Cyber-Physical System in the Automotive Domain. 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :326–333.
Software development for Cyber-Physical Systems (CPS), e.g., autonomous vehicles, requires both functional and non-functional quality assurance to guarantee that the CPS operates safely and effectively. EAST-ADL is a domain specific architectural language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time (ERT) behaviors modeled in EAST-ADL/Stateflow into UPPAAL models amenable to formal verification. Previous work is extended in this paper by including support for Simulink and an integration of Simulink/Stateflow (S/S) within the same too lchain. S/S models are transformed, based on the extended ERT constraints with probability parameters, into verifiable UPPAAL-SMC models and integrate the translation with formal statistical analysis techniques: Probabilistic extension of EAST-ADL constraints is defined as a semantics denotation. A set of mapping rules is proposed to facilitate the guarantee of translation. Formal analysis on both functional- and non-functional properties is performed using Simulink Design Verifier and UPPAAL-SMC. Our approach is demonstrated on the autonomous traffic sign recognition vehicle case study.