Visible to the public Biblio

Filters: Keyword is verification  [Clear All Filters]
2021-08-02
Abdul Basit Ur Rahim, Muhammad, Duan, Qi, Al-Shaer, Ehab.  2020.  A Formal Analysis of Moving Target Defense. 2020 IEEE 44th Annual Computers, Software, and Applications Conference (COMPSAC). :1802—1807.
Static system configuration provides a significant advantage for the adversaries to discover the assets and launch attacks. Configuration-based moving target defense (MTD) reverses the cyber warfare asymmetry by mutating certain configuration parameters to disrupt the attack planning or increase the attack cost significantly. In this research, we present a methodology for the formal verification of MTD techniques. We formally modeled MTD techniques and verified them against constraints. We use Random Host Mutation (RHM) as a case study for MTD formal verification. The RHM transparently mutates the IP addresses of end-hosts and turns into untraceable moving targets. We apply the formal methodology to verify the correctness, safety, mutation, mutation quality, and deadlock-freeness of RHM using the model checking tool. An adversary is also modeled to validate the effectiveness of the MTD technique. Our experimentation validates the scalability and feasibility of the formal verification methodology.
2021-05-03
Naik, Nikhil, Nuzzo, Pierluigi.  2020.  Robustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems. 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). :1–12.
The proliferation of artificial intelligence based systems in all walks of life raises concerns about their safety and robustness, especially for cyber-physical systems including multiple machine learning components. In this paper, we introduce robustness contracts as a framework for compositional specification and reasoning about the robustness of cyber-physical systems based on neural network (NN) components. Robustness contracts can encompass and generalize a variety of notions of robustness which were previously proposed in the literature. They can seamlessly apply to NN-based perception as well as deep reinforcement learning (RL)-enabled control applications. We present a sound and complete algorithm that can efficiently verify the satisfaction of a class of robustness contracts on NNs by leveraging notions from Lagrangian duality to identify system configurations that violate the contracts. We illustrate the effectiveness of our approach on the verification of NN-based perception systems and deep RL-based control systems.
Wu, Shanglun, Yuan, Yujie, Kar, Pushpendu.  2020.  Lightweight Verification and Fine-grained Access Control in Named Data Networking Based on Schnorr Signature and Hash Functions. 2020 IEEE 20th International Conference on Communication Technology (ICCT). :1561–1566.
Named Data Networking (NDN) is a new kind of architecture for future Internet, which is exactly satisfied with the rapidly increasing mobile requirement and information-depended applications that dominate today's Internet. However, the current verification-data accessed system is not safe enough to prevent data leakage because no strongly method to resist any device or user to access it. We bring up a lightweight verification based on hash functions and a fine-grained access control based on Schnorr Signature to address the issue seamlessly. The proposed scheme is scalable and protect data confidentiality in a NDN network.
Paulsen, Brandon, Wang, Jingbo, Wang, Jiawei, Wang, Chao.  2020.  NEURODIFF: Scalable Differential Verification of Neural Networks using Fine-Grained Approximation. 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE). :784–796.
As neural networks make their way into safety-critical systems, where misbehavior can lead to catastrophes, there is a growing interest in certifying the equivalence of two structurally similar neural networks - a problem known as differential verification. For example, compression techniques are often used in practice for deploying trained neural networks on computationally- and energy-constrained devices, which raises the question of how faithfully the compressed network mimics the original network. Unfortunately, existing methods either focus on verifying a single network or rely on loose approximations to prove the equivalence of two networks. Due to overly conservative approximation, differential verification lacks scalability in terms of both accuracy and computational cost. To overcome these problems, we propose NEURODIFF, a symbolic and fine-grained approximation technique that drastically increases the accuracy of differential verification on feed-forward ReLU networks while achieving many orders-of-magnitude speedup. NEURODIFF has two key contributions. The first one is new convex approximations that more accurately bound the difference of two networks under all possible inputs. The second one is judicious use of symbolic variables to represent neurons whose difference bounds have accumulated significant error. We find that these two techniques are complementary, i.e., when combined, the benefit is greater than the sum of their individual benefits. We have evaluated NEURODIFF on a variety of differential verification tasks. Our results show that NEURODIFF is up to 1000X faster and 5X more accurate than the state-of-the-art tool.
2020-10-26
Criswell, John, Zhou, Jie, Gravani, Spyridoula, Hu, Xiaoyu.  2019.  PrivAnalyzer: Measuring the Efficacy of Linux Privilege Use. 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). :593–604.
Operating systems such as Linux break the power of the root user into separate privileges (which Linux calls capabilities) and give processes the ability to enable privileges only when needed and to discard them permanently when the program no longer needs them. However, there is no method of measuring how well the use of such facilities reduces the risk of privilege escalation attacks if the program has a vulnerability. This paper presents PrivAnalyzer, an automated tool that measures how effectively programs use Linux privileges. PrivAnalyzer consists of three components: 1) AutoPriv, an existing LLVM-based C/C++ compiler which uses static analysis to transform a program that uses Linux privileges into a program that safely removes them when no longer needed, 2) ChronoPriv, a new LLVM C/C++ compiler pass that performs dynamic analysis to determine for how long a program retains various privileges, and 3) ROSA, a new bounded model checker that can model the damage a program can do at each program point if an attacker can exploit the program and abuse its privileges. We use PrivAnalyzer to determine how long five privileged open source programs retain the ability to cause serious damage to a system and find that merely transforming a program to drop privileges does not significantly improve security. However, we find that simple refactoring can considerably increase the efficacy of Linux privileges. In two programs that we refactored, we reduced the percentage of execution in which a device file can be read and written from 97% and 88% to 4% and 1%, respectively.
2020-10-16
Babenko, Liudmila, Pisarev, Ilya.  2018.  Security Analysis of the Electronic Voting Protocol Based on Blind Intermediaries Using the SPIN Verifier. 2018 International Conference on Cyber-Enabled Distributed Computing and Knowledge Discovery (CyberC). :43—435.

Cryptographic protocols are the basis for the security of any protected system, including the electronic voting system. One of the most effective ways to analyze protocol security is to use verifiers. In this paper, the formal verifier SPIN was used to analyze the security of the cryptographic protocol for e-voting, which is based on model checking using linear temporal logic (LTL). The cryptographic protocol of electronic voting is described. The main structural units of the Promela language used for simulation in the SPIN verifier are described. The model of the electronic voting protocol in the language Promela is given. The interacting parties, transferred data, the order of the messages transmitted between the parties are described. Security of the cryptographic protocol using the SPIN tool is verified. The simulation of the protocol with active intruder using the man in the middle attack (MITM) to substitute data is made. In the simulation results it is established that the protocol correctly handles the case of an active attack on the parties' authentication.

2020-10-05
Kanellopoulos, Aris, Vamvoudakis, Kyriakos G., Gupta, Vijay.  2019.  Decentralized Verification for Dissipativity of Cascade Interconnected Systems. 2019 IEEE 58th Conference on Decision and Control (CDC). :3629—3634.

In this paper, we consider the problem of decentralized verification for large-scale cascade interconnections of linear subsystems such that dissipativity properties of the overall system are guaranteed with minimum knowledge of the dynamics. In order to achieve compositionality, we distribute the verification process among the individual subsystems, which utilize limited information received locally from their immediate neighbors. Furthermore, to obviate the need for full knowledge of the subsystem parameters, each decentralized verification rule employs a model-free learning structure; a reinforcement learning algorithm that allows for online evaluation of the appropriate storage function that can be used to verify dissipativity of the system up to that point. Finally, we show how the interconnection can be extended by adding learning-enabled subsystems while ensuring dissipativity.

2020-09-14
Lochbihler, Andreas, Sefidgar, S. Reza, Basin, David, Maurer, Ueli.  2019.  Formalizing Constructive Cryptography using CryptHOL. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :152–15214.
Computer-aided cryptography increases the rigour of cryptographic proofs by mechanizing their verification. Existing tools focus mainly on game-based proofs, and efforts to formalize composable frameworks such as Universal Composability have met with limited success. In this paper, we formalize an instance of Constructive Cryptography, a generic theory allowing for clean, composable cryptographic security statements. Namely, we extend CryptHOL, a framework for game-based proofs, with an abstract model of Random Systems and provide proof rules for their equality and composition. We formalize security as a special kind of system construction in which a complex system is built from simpler ones. As a simple case study, we formalize the construction of an information-theoretically secure channel from a key, a random function, and an insecure channel.
2020-06-22
Kasodhan, Rashmi, Gupta, Neetesh.  2019.  A New Approach of Digital Signature Verification based on BioGamal Algorithm. 2019 3rd International Conference on Computing Methodologies and Communication (ICCMC). :10–15.
In recent times, online services are playing a crucial role in our day-to-day life applications. Inspite of their advantage, it also have certain security challenges in the communication network. Security aspects consists of authentication of users, confidentiality of data/information as well as integrity of data. In order to achieve all these parameters, the sensitive information must be digitally signed by the original sender and later verified by the intended recipient. Therefore, research on digital signatures should be further developed to improve the data security and authenticity of the transferred data. In this paper, a secured digital signature algorithm is designed. The design of secure digital signature uses the concept of hybridization of secure hash code, DNA encryption/decryption technique and elgamal encryption/decryption techniques. The use of SHA algorithm generates a secure hash code and hybridization of encryption algorithm reduces the computational complexity and this research method is then compared with existing PlayGamal algorithm with respect to encryption/decryption time complexity.
2020-06-01
Laranjeiro, Nuno, Gomez, Camilo, Schiavone, Enrico, Montecchi, Leonardo, Carvalho, Manoel J. M., Lollini, Paolo, Micskei, Zoltán.  2019.  Addressing Verification and Validation Challenges in Future Cyber-Physical Systems. 2019 9th Latin-American Symposium on Dependable Computing (LADC). :1–2.
Cyber-physical systems are characterized by strong interactions between their physical and computation parts. The increasing complexity of such systems, now used in numerous application domains (e.g., aeronautics, healthcare), in conjunction with hard to predict surrounding environments or the use of non-traditional middleware and with the presence of non-deterministic or non-explainable software outputs, tend to make traditional Verification and Validation (V&V) techniques ineffective. This paper presents the H2020 ADVANCE project, which aims precisely at addressing the Verification and Validation challenges that the next-generation of cyber-physical systems bring, by exploring techniques, methods and tools for achieving the technical objective of improving the overall efficiency and effectiveness of the V&V process. From a strategic perspective, the goal of the project is to create an international network of expertise on the topic of V&V of cyber-physical systems.
2020-04-03
Cheang, Kevin, Rasmussen, Cameron, Seshia, Sanjit, Subramanyan, Pramod.  2019.  A Formal Approach to Secure Speculation. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF). :288—28815.
Transient execution attacks like Spectre, Meltdown and Foreshadow have shown that combinations of microarchitectural side-channels can be synergistically exploited to create side-channel leaks that are greater than the sum of their parts. While both hardware and software mitigations have been proposed against these attacks, provable security has remained elusive. This paper introduces a formal methodology for enabling secure speculative execution on modern processors. We propose a new class of information flow security properties called trace property-dependent observational determinism (TPOD). We use this class to formulate a secure speculation property. Our formulation precisely characterises all transient execution vulnerabilities. We demonstrate its applicability by verifying secure speculation for several illustrative programs.
Lipp, Benjamin, Blanchet, Bruno, Bhargavan, Karthikeyan.  2019.  A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. 2019 IEEE European Symposium on Security and Privacy (EuroS P). :231—246.

WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocol underlying WireGuard, using the CryptoVerif proof assistant. We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard. Our work also provides novel theoretical contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in popular Diffie-Hellman groups like Curve25519, which is used in many modern protocols including WireGuard. To our knowledge, this is the first mechanised cryptographic proof for any protocol employing such a precise model. Second, we prove several indifferentiability lemmas that are useful to simplify the proofs for sequences of key derivations.

2020-03-30
Ahamed, Md. Salahuddin, Asiful Mustafa, Hossen.  2019.  A Secure QR Code System for Sharing Personal Confidential Information. 2019 International Conference on Computer, Communication, Chemical, Materials and Electronic Engineering (IC4ME2). :1–4.
Securing and hiding personal confidential information has become a challenge in these modern days. Due to the lack of security and confidentiality, forgery of confidential information can cause a big margin loss to a person. Personal confidential information needs to be securely shared and hidden with the expected recipient and he should be able to verify the information by checking its authenticity. QR codes are being used increasingly to share data for different purposes. In information communication, QR code is important because of its high data capacity. However, most existing QR code systems use insecure data format and encryption is rarely used. A user can use Secure QR Code (SQRC) technology to keep information secured and hidden. In this paper, we propose a novel SQRC system which will allow sharing authentic personal confidential information by means of QR code verification using RSA digital signature algorithm and also allow authorizing the information by means of QR code validation using RSA public key cryptographic algorithm. We implemented the proposed SQRC system and showed that the system is effective for sharing personal confidential information securely.
2020-03-18
Ye, Fanghan, Dong, Xiaolei, Shen, Jiachen, Cao, Zhenfu, Zhao, Wenhua.  2019.  A Verifiable Dynamic Multi-user Searchable Encryption Scheme without Trusted Third Parties. 2019 IEEE 25th International Conference on Parallel and Distributed Systems (ICPADS). :896–900.
Searchable encryption is a cryptographic primitive that allows users to search for keywords on encrypted data. It allows users to search in archives stored on cloud servers. Among searchable encryption schemes, those supporting multiuser settings are more suitable for daily application scenarios and more practical. However, since the cloud server is semi-trusted, the result set returned by the server is undefined, and most existing multi-user searchable encryption schemes rely heavily on trusted third parties to manage user permission. To address these problems, verifiable multi-user searchable encryption schemes with dynamic management of user search permissions, weak trust on trusted third parties and are desirable. In this paper, we propose such a scheme. Our scheme manages user permission and key distribution without a trusted third party. User search permission and user access permission matrices are generated separately to manage user permissions dynamically. In addition, our scheme can verify the result set returned by the cloud server. We also show that our scheme is index and trapdoor indistinguishable under chosen keyword attacks in the random oracle model. Finally, a detailed comparison experiment is made by using the actual document data set, and the results show that our scheme is efficient and practical.
2020-03-16
Noori-Hosseini, Mona, Lennartson, Bengt.  2019.  Incremental Abstraction for Diagnosability Verification of Modular Systems. 2019 24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). :393–399.
In a diagnosability verifier with polynomial complexity, a non-diagnosable system generates uncertain loops. Such forbidden loops are in this paper transformed to forbidden states by simple detector automata. The forbidden state problem is trivially transformed to a nonblocking problem by considering all states except the forbidden ones as marked states. This transformation is combined with one of the most efficient abstractions for modular systems called conflict equivalence, where nonblocking properties are preserved. In the resulting abstraction, local events are hidden and more local events are achieved when subsystems are synchronized. This incremental abstraction is applied to a scalable production system, including parallel lines where buffers and machines in each line include some typical failures and feedback flows. For this modular system, the proposed diagnosability algorithm shows great results, where diagnosability of systems including millions of states is analyzed in less than a second.
Goli, Mehran, Drechsler, Rolf.  2019.  Scalable Simulation-Based Verification of SystemC-Based Virtual Prototypes. 2019 22nd Euromicro Conference on Digital System Design (DSD). :522–529.
Virtual Prototypes (VPs) at the Electronic System Level (ESL) written in SystemC language using its Transaction Level Modeling (TLM) framework are increasingly adopted by the semiconductor industry. The main reason is that VPs are much earlier available, and their simulation is orders of magnitude faster in comparison to the hardware models implemented at lower levels of abstraction (e.g. RTL). This leads designers to use VPs as reference models for an early design verification. Hence, the correctness assurance of these reference models (VPs) is critical as undetected faults may propagate to less abstract levels in the design process, increasing the fixing cost and effort. In this paper, we propose a novel simulation-based verification approach to automatically validate the simulation behavior of a given SystemC VP against both the TLM-2.0 rules and its specifications (i.e. functional and timing behavior of communications in the VP). The scalability and the efficiency of the proposed approach are demonstrated using an extensive set of experiments including a real-word VP.
2020-03-02
Zhao, Zhijun, Jiang, Zhengwei, Wang, Yueqiang, Chen, Guoen, Li, Bo.  2019.  Experimental Verification of Security Measures in Industrial Environments. 2019 IEEE International Conference on Computational Science and Engineering (CSE) and IEEE International Conference on Embedded and Ubiquitous Computing (EUC). :498–502.
Industrial Control Security (ICS) plays an important role in protecting Industrial assets and processed from being tampered by attackers. Recent years witness the fast development of ICS technology. However there are still shortage of techniques and measures to verify the effectiveness of ICS approaches. In this paper, we propose a verification framework named vICS, for security measures in industrial environments. vICS does not requires installing any agent in industrial environments, and could be viewed as a non-intrusive way. We use vICS to evaluate the effectiveness of classic ICS techniques and measures through several experiments. The results shown that vICS provide an feasible solution for verifying the effectiveness of classic ICS techniques and measures for industrial environments.
2019-12-02
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.
2019-11-12
Xiao, Lili, Xiang, Shuangqing, Zhuy, Huibiao.  2018.  Modeling and Verifying SDN with Multiple Controllers. Proceedings of the 33rd Annual ACM Symposium on Applied Computing. :419-422.

SDN (Software Defined Network) with multiple controllers draws more attention for the increasing scale of the network. The architecture can handle what SDN with single controller is not able to address. In order to understand what this architecture can accomplish and face precisely, we analyze it with formal methods. In this paper, we apply CSP (Communicating Sequential Processes) to model the routing service of SDN under HyperFlow architecture based on OpenFlow protocol. By using model checker PAT (Process Analysis Toolkit), we verify that the models satisfy three properties, covering deadlock freeness, consistency and fault tolerance.

2019-06-28
Tsankov, Petar, Dan, Andrei, Drachsler-Cohen, Dana, Gervais, Arthur, Bünzli, Florian, Vechev, Martin.  2018.  Securify: Practical Security Analysis of Smart Contracts. Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. :67-82.

Permissionless blockchains allow the execution of arbitrary programs (called smart contracts), enabling mutually untrusted entities to interact without relying on trusted third parties. Despite their potential, repeated security concerns have shaken the trust in handling billions of USD by smart contracts. To address this problem, we present Securify, a security analyzer for Ethereum smart contracts that is scalable, fully automated, and able to prove contract behaviors as safe/unsafe with respect to a given property. Securify's analysis consists of two steps. First, it symbolically analyzes the contract's dependency graph to extract precise semantic information from the code. Then, it checks compliance and violation patterns that capture sufficient conditions for proving if a property holds or not. To enable extensibility, all patterns are specified in a designated domain-specific language. Securify is publicly released, it has analyzed 18K contracts submitted by its users, and is regularly used to conduct security audits by experts. We present an extensive evaluation of Securify over real-world Ethereum smart contracts and demonstrate that it can effectively prove the correctness of smart contracts and discover critical violations.

Liu, Jed, Hallahan, William, Schlesinger, Cole, Sharif, Milad, Lee, Jeongkeun, Soulé, Robert, Wang, Han, Ca\c scaval, C\u alin, McKeown, Nick, Foster, Nate.  2018.  P4V: Practical Verification for Programmable Data Planes. Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. :490-503.

We present the design and implementation of p4v, a practical tool for verifying data planes described using the P4 programming language. The design of p4v is based on classic verification techniques but adds several key innovations including a novel mechanism for incorporating assumptions about the control plane and domain-specific optimizations which are needed to scale to large programs. We present case studies showing that p4v verifies important properties and finds bugs in real-world programs. We conduct experiments to quantify the scalability of p4v on a wide range of additional examples. We show that with just a few hundred lines of control-plane annotations, p4v is able to verify critical safety properties for switch.p4, a program that implements the functionality of on a modern data center switch, in under three minutes.

2019-06-10
Li, T., Ma, J., Pei, Q., Shen, Y., Sun, C..  2018.  Log-based Anomalies Detection of MANETs Routing with Reasoning and Verification. 2018 Asia-Pacific Signal and Information Processing Association Annual Summit and Conference (APSIPA ASC). :240–246.

Routing security plays an important role in Mobile Ad hoc Networks (MANETs). Despite many attempts to improve its security, the routing procedure of MANETs remains vulnerable to attacks. Existing approaches offer support for detecting attacks or debugging in different routing phases, but many of them have not considered the privacy of the nodes during the anomalies detection, which depend on the central control program or a third party to supervise the whole network. In this paper, we present an approach called LAD which uses the raw logs of routers to construct control a flow graph and find the existing communication rules in MANETs. With the reasoning rules, LAD can detect both active and passive attacks launched during the routing phase. LAD can also protect the privacy of the nodes in the verification phase with the specific Merkle hash tree. Without deploying any special nodes to assist the verification, LAD can detect multiple malicious nodes by itself. To show that our approach can be used to guarantee the security of the MANETs, we deploy our experiment in NS3 as well as the practical router environment. LAD can improve the accuracy rate from 2.28% to 29.22%. The results show that LAD performs limited time and memory usages, high detection and low false positives.

2019-03-15
Keshishzadeh, Sarineh, Fallah, Ali, Rashidi, Saeid.  2018.  Electroencephalogram Based Biometrics: A Fractional Fourier Transform Approach. Proceedings of the 2018 2Nd International Conference on Biometric Engineering and Applications. :1-5.
The non-stationary nature of the human Electroencephalogram (EEG) has caused problems in EEG based biometrics. Stationary signals analysis is done simply with Discrete Fourier Transform (DFT), while it is not possible to analyze non-stationary signals with DFT, as it does not have the ability to show the occurrence time of different frequency components. The Fractional Fourier Transform (FrFT), as a generalization of Fourier Transform (FT), has the ability to exhibit the variable frequency nature of non-stationary signals. In this paper, Discrete Fractional Fourier Transform (DFrFT) with different fractional orders is proposed as a novel feature extraction technique for EEG based human verification with different number of channels. The proposed method in its' best performance achieved 0.22% Equal Error Rate (EER) with three EEG channels of 104 subjects.
2019-01-31
Abou-Zahra, Shadi, Brewer, Judy, Cooper, Michael.  2018.  Artificial Intelligence (AI) for Web Accessibility: Is Conformance Evaluation a Way Forward? Proceedings of the Internet of Accessible Things. :20:1–20:4.

The term "artificial intelligence" is a buzzword today and is heavily used to market products, services, research, conferences, and more. It is scientifically disputed which types of products and services do actually qualify as "artificial intelligence" versus simply advanced computer technologies mimicking aspects of natural intelligence. Yet it is undisputed that, despite often inflationary use of the term, there are mainstream products and services today that for decades were only thought to be science fiction. They range from industrial automation, to self-driving cars, robotics, and consumer electronics for smart homes, workspaces, education, and many more contexts. Several technological advances enable what is commonly referred to as "artificial intelligence". It includes connected computers and the Internet of Things (IoT), open and big data, low cost computing and storage, and many more. Yet regardless of the definition of the term artificial intelligence, technological advancements in this area provide immense potential, especially for people with disabilities. In this paper we explore some of these potential in the context of web accessibility. We review some existing products and services, and their support for web accessibility. We propose accessibility conformance evaluation as one potential way forward, to accelerate the uptake of artificial intelligence, to improve web accessibility.

2018-08-23
Zave, Pamela, Ferreira, Ronaldo A., Zou, Xuan Kelvin, Morimoto, Masaharu, Rexford, Jennifer.  2017.  Dynamic Service Chaining with Dysco. Proceedings of the Conference of the ACM Special Interest Group on Data Communication. :57–70.
Middleboxes are crucial for improving network security and performance, but only if the right traffic goes through the right middleboxes at the right time. Existing traffic-steering techniques rely on a central controller to install fine-grained forwarding rules in network elements—at the expense of a large number of rules, a central point of failure, challenges in ensuring all packets of a session traverse the same middleboxes, and difficulties with middleboxes that modify the "five tuple." We argue that a session-level protocol is a fundamentally better approach to traffic steering, while naturally supporting host mobility and multihoming in an integrated fashion. In addition, a session-level protocol can enable new capabilities like dynamic service chaining, where the sequence of middleboxes can change during the life of a session, e.g., to remove a load-balancer that is no longer needed, replace a middlebox undergoing maintenance, or add a packet scrubber when traffic looks suspicious. Our Dysco protocol steers the packets of a TCP session through a service chain, and can dynamically reconfigure the chain for an ongoing session. Dysco requires no changes to end-host and middlebox applications, host TCP stacks, or IP routing. Dysco's distributed reconfiguration protocol handles the removal of proxies that terminate TCP connections, middleboxes that change the size of a byte stream, and concurrent requests to reconfigure different parts of a chain. Through formal verification using Spin and experiments with our Linux-based prototype, we show that Dysco is provably correct, highly scalable, and able to reconfigure service chains across a range of middleboxes.