Accountable Software Systems

Computerised systems are increasingly opaque, due to their size and to the nature of the new AI systems, such as neural networks. Yet, we have to be able to reason about the correctness of these systems, debug them, fix errors, answer “what if” questions, and explain their decisions. In this talk, I present a framework for causal explanations of image classifiers, based on the notions of actual causality and explainability. Our tool ReX provides explanations that approximate minimal subsets of the image sufficient to get the same classification if the rest of the image is hidden. I describe our recent work in extending ReX to multiple explanations and survey the challenges in adapting the existing explainability tools to medical applications.

Recent digital rights frameworks stipulate an ability to request that a data controller – roughly, any system that stores and manipulates personal information – “erase” or “delete” one’s data (e.g., the “right to be forgotten” in the GDPR). We ask how deletion should be formalized in complex systems that interact with many parties and store derivative information. There are two broad principles at work in existing approaches to formalizing deletion: confidentiality and control. This talk briefly explores these questions in the specific context of machine learning models, and erasing training data therefrom.

This talk began with a quick overview of the regulatory landscape for aviation. Today, there are distinctly different regulatory process paths for hardware/software system components and for the human operators and their roles in the overall system. Today, the handling of almost all remaining uncertainty is pushed into the operational assurance processes. This means that hardware and software components are expected to be highly deterministic. As we increasingly push required system functionality from execution by people into execution by automation we are running into the limits of what our current processes allow us to assure. This is broadly perceived as a barrier to innovation.

One way forward could be a shift to assurance models that merge and blend our current paradigms for silicon-based and human-based assurance.

We draw inspiration from the field of system safety to understand challenges with accountability in the development, use and governance of software systems. System safety has dealt with accidents and harm in safety-critical systems subject to varying degrees of software-based automation, already for many decades. As a result, it has some crystallized lessons, tools and ontologies that establish conditions for accountability to promote or guarantee safety, as well as to inform the design of actual mechanisms for accountability. We covered two core concepts that capture such conditions and mechanisms. At the operational level, the process model which details the goals, constraints, actions, observations and models/knowledge needed to safely operate processes subject to software-based automation. At the organizational and institutional levels, the safety control structure combines, describes and relates all mechanisms contributing to safety, including the operational mechnisms, and extending towards managerial, maintenance and research and development. Moving further up, the control structure also includes various regulatory, policy, advocacy law-making, law-enforcing and judicial mechanisms. System safety methods allow for the integral analysis of unsafe or otherwise undesirable behaviors and outcomes in software systems, helping to understand how various mechanisms contribute to material outcomes, either directly in a causal sense or indirectly by providing the environmental factors for such system behavior and outcomes to emerge. We concluded with a few lessons written down in Nancy Leveson’s magnum opus “Engineering a Safer World: Systems Thinking Applied to Safety”, including the curse of flexibility and the crucial importance of culture in upholding accountability mechanisms.

This firestarter talk was a brief “teaser” of the work in [1].

Accountability is a widely studied but amorphous concept, used to mean different things across different disciplines and domains of application. Here, we survey work on accountability in computer science and other disciplines. We motivate our survey with a study of the myriad ways in which the term “accountability” has been used across disciplines and the concepts that play key roles in defining it. This leads us to identify a temporal spectrum onto which we may place different notions of accountability to facilitate their comparison. We then survey accountability mechanisms for different application domains in computer science and place them on our spectrum. Building on this broader survey, we review frameworks and languages for studying accountability in computer science. Finally, we offer conclusions, open questions, and future directions.

A number of scholars ahve identified the complexity of locating organisational accountability in AI products because of complex industrial arrangements. But there are similar complexities in the dataset supply chain for AI models. Datasets used to train commercial and noncommercial models are produced and refined by numerous organisations with different characteristics and for different purposes. These inter-organisational forms of coordination and strategic partnership result in complex “ecologies” of data flow subject to complex forms of regulatory arbitrage. But what kind of “ecology” is this? Inspired by the work of Anna Tsing, the goals here is to understand or conceptualise these mutualistic relations and multi-organisational associations, the data flows they coordinate, and the products they produce as a type of mushroom, whose arrangement depends on a broader political economy.

Case management and business processes regulated by law are increasingly being digitalized, in the public as well as the private sector. At the same time, laws are continuously changed and new regulations are introduced. Moreover, law needs to be open for interpretation and re-interpretation. This calls for new methods to ensure accountability of the legal decision support. We present the DCR Graph tools and notation developed and tested in the EcoKnow.org project, which allows domain experts to map the law to a DCR Graph (which is essentially a temporal logic knowledge graph) and validate the meaning through simulation. Via the tools developed by the research-based company DCR Solutions, the graphs can be used to provide dynamic guidelines, case management support and automation, and is used widely in the public sector in Denmark via the KMD WorkZone Enterprise Information Management system.

This talk examines why the “platform” model is crucial to thinking about software accountability. Software production, deployment and use is increasingly intermediated through the organisational form of the “platform” – generally private entities which control access to computational resources as well as structure and organise the “market” for software products. Through varying levels of control over elements of a software production or deployment “stack”, the platform model is crucial for thinking about accountability in software production.

As platforms increasingly determine access to computational resources and the ability to run softwares, they exercise power over users or populations in ways that may be undemocratic or unjust. Smartphone OS providers can arbitrarily expand the surveillance capabilities of mobile devices or IoT devices, and “App Stores” can similarly chose to unilaterally force changes to software production business models, as we have seen in the recent past.

This also places limits on how we can democratically and legitimately control computation and software production or use that is increasingly “infrastructural”, i.e. a common, shared resource that is vital for conducting an array of activities. Given that these infrastructures are globally distributed and usually privately controlled, nation states or other legitimate publics have little insight or control into how governance decisions are made on platforms. At the level of the state, this is also giving rise to calls for expanding upon “digital sovereignty” through a number of measures, including regulation, or creating public alternatives.

Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal philosophy offers a paramount method for assessing culpability: putting the agent “on the stand” to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding. We use the formal methods of symbolic execution and satisfiability modulo theories (SMT) solving to discharge queries about agent behavior in factual and counterfactual scenarios, as adaptively formulated by a human investigator. We implement our framework and demonstrate its utility on an illustrative car crash scenario.

Although algorithms are imbued with a sense of objectivity and reliability, numerous high-profile incidents have demonstrated their fallibility. Despite their ubiquity, access to algorithms and algorithmic systems is typically policed, meaning that our understanding of what it is that people who develop algorithms “do” and why algorithms fail in practice remains largely unexplored. In a way, these systems that are designed for structuring and ordering, themselves often resist straightforward categorization and control. This observation echoes Seaver’s concept [3] of software systems as “culturally enacted” through user interaction, challenging the notion of these systems as fixed technical objects. My approach, while similar in nature to Seaver’s, took a slightly different point of departure. Specifically, I built on studies by Beunza and Garud [1], Beunza and Stark [2], and Spears [4] that – like Seaver – center on understanding the socio-material context of algorithms. However, such work in the Social Studies of Finance domain also focuses on understanding the “technical” aspects of algorithms themselves. In a recent case study, I investigate the development – and demise – of an algorithmic system that used Wi-Fi data as an input for footfall measurement in the Netherlands. The study utilizes an ethnographic approach to track the development and eventual abandonment of this system that measured footfall in 1100 locations across the Netherlands. Based on the case study I conclude that, in comparison to the manual collection of footfall measurement, the transition to more digital modes of data collection has several unique characteristics that matter for the processes of knowledge production: 1. The speed and volume of these new modes of data collection is much higher; 2. The new modes of data collection are relatively untried, hard to calibrate, and in general more error-prone; 3. New modes of data collection can be – and are – contested on the basis of non-digital observations. In unison this leads to the – attempted- alignment of divergent measures of footfall and integration previously isolated epistemic cultures. In pursuit of more understanding of – and more influence over – algorithmic systems, ethnographic studies like these may contribute by shedding light on the mundane practices of those involved in their development and use.

The Tamarin [1] protocol verification tool (https://tamarin-prover.github.io/) integrates support for verifying protocol accountability in the following sense: “protocol provides accountability for property iff, at all times, the protocol can correctly determine the parties causing violation of this property”. We first explain that we need causation to define this property, and that, more precisely, causes ought to be the fact whether or whether not a party deviated from protocol behavior. Then we outline how this is done, and how this technique developed to support an unbounded number of parties. We talk about the case studies we performed and demonstrate the Tamarin tool and its web GUI.

With the onset of the global pandemic in early 2020 came a massive push to deploy digital technologies to aid in pandemic mitigation. In this talk, we looked back at how the DP3T project proposed a privacy-friendly approach to digital contact tracing [1], eventually leading to its adoption by Google and Apple. This adoption was an essential enabler of the use of these technologies, but also surfaces questions of accountability. What does it mean to design solutions on such a short timescale? How can citizens convince themselves that the privacy protections are implemented as designed? And what does it mean for Google and Apple to control what health applications can and cannot do [2]?

How French government agencies explain decisions taken by an IT system following the law? Typical example is the amount of taxes and social benefit you get/pay once you’ve filled the form. With several other authors, we have done : a state of the art, interviews with social workers and social benefits agency agents about what use they have for explainability, how this plays out with respect to accountability, and prototyping automatic generation of law-based explanations using the Catala programming language.

Investigated model of transparency, in french law you have to publish the source code. In the case of housing benefits distributed by CNAF, cobol code from 1995, unreadable. So that is a problem. French law forces them to publish a summary of what the algorithm is doing but you can’t condense 300 pages in 2-pages that they published, if you add all the edge cases together you get the entire population. Last requirement, for each decision that is made by an algo you should provide a detailed, individualize, and legible explanation. We looked at all the govt systems that should provide these, but none of them do. From there, we wanted to investigate deeper on the housing benefits case and interviewed social workers and CNAF agents about their use of explainability of decisions. Findings: low-level social workers completely trust the algorithm, higher-level workers sort of understand the principles of how it works but without being able to link the behavior to the law that specifies it. To contest it, detect an algorithm error or debug it you need link between law and code through a detailed explanation of how thing was computed. However at CNAF there’s a lenghty process between law and code with two different specification/documentation sets written by different groups of people. Recommendation : you should be able to link the law, the code and the explanations of how the code executed, while automatically producing explanations and sharing them externally to have more accurate contestations from the outside for maybe better debugging of the algorithm.

When using automated decision-making systems (ADM systems) in the public sector, authorities act in a unique context and bear special responsibilities towards the people affected. Against this background, the use of ADM systems by public administrations should be subject to stringent transparency mechanisms – including public registers and mandatory impact assessments.

Without the ability to know whether ADM systems are being deployed, all other efforts for the reconciliation of fundamental rights and ADM systems are doomed to fail. Legally mandatory public registers of all ADM systems used by public administrations – at communal, regional, national, and supranational levels – should therefore be created.

These registers should come with the legal obligation for those responsible for the ADM system to disclose information on the underlying model of the system, its developers and deployers, the purpose of its use, and the results of the algorithmic impact assessment.

In order to make a difference in practice, ethical reflection must be translated into ready-to-use tools, providing authorities with the means for conducting such an analysis. To this end, we have developed a practical, user-friendly, and concrete impact assessment tool, enabling the evaluation of an ADM system throughout its entire life cycle.

If you’d like to add bibliographic references to your abstract, please use the thebibliography-environment (bibtex-files are not supported):

Looking on responsibility and liability regarding software and especially non-symbolic artificial intelligence from the legal perspective, I start with two distinctions. The first one regards the different branches of law. Public law and especially administrative law concentrate on prohibitions and permissions and criminal law on prohibitions as well. Both necessarily involve the state as such and are mainly statute law. Private law relates to private individuals. Contract law allows the private shaping of law. Tort law regulates compensation for damages on a non-contractual basis. The second distinction is between general and special purpose law. With regard to software there is law aiming at software or digitalization at large like – in the context of the EU – the General Data Protection Regulation, the Digital Markets Act and the Digital Service Act as well as the proposals for an AI Act and an AI Liability Directive. There is also special law in more general statutes like computer fraud in the criminal code or the provisions regarding consumer contracts on digital products in the civil code, that lead to a convergence between software contracts based on the law of sale and those based on rental or service contracts. But software and digitalization at large are also covered by law not directly aiming at them like competition law, ordinary fraud, most of contract law or tort law. Regarding software there are legal relationships between a lot of actors. In general, it starts with a contract between the producer and the user, very often intermediated by a provider or dealer. Often, there is another contract between the user and his client, like a medical practitioner and his patient. On the other end of the chain there are contracts between the producer and his suppliers, like the programmer, the data supplier or trainers. In case of damage, there are non-contractual relationships based on tort governing the compensation. They exist in parallel to the contractual relationships but also independent to these and to especially third parties. My talk concerns responsibility and liability regarding software and especially artificial intelligence concentrated on tort law. Tort law is the branch of private law concerned with the award of compensation for damages even if there is no contractual relationship between the damaging and the damaged party. Basically, tort law is no law designed especially for information technology and digitalization, but general-purpose law. As such it is the part of law very often concerned first with new developments. The most relevant branch of tort law in this context is product liability. The conditions for product liability based on negligence in essential are an infringement of legal interests, a breach of duty of care or conduct and causation. Based on strict liability they are an infringement of legal interest, being active in a specific domain, like road traffic or gene technology, and causation. The difference is, that there is no need to define a duty under strict liability. But there exist exemptions to strict liability with similar effects but being much more defined. Product liability claims can be based on both, negligence and strict liability. They require a defective product that does not provide the safety to expect and causes damages to specified legal interest not comprising pure economic loss. In our context the most relevant defects are design defects and instruction defects. Design defects can be identified form a bird’s eye perspective by comparing the product to other products or from a frog perspective by looking whether a specific feature could have been better. Instruction defects fail to inform the users properly, especially to warn of risks. An interesting question is, whether and when flaws in the design can be compensated for by instructions or warnings. In this respect, design and instruction defects are a sort of communicating vessels between the producer and the user and could shift risks between them. The level of safety depends on what is technically possible and on the risks involved. The more risky a product is, the higher the product safety requirements. In extreme cases, the necessary safety level cannot be achieved. This mechanism is also known in other areas of law and is also the basis of the AI Act. In the end, the concrete level of safety to be provided has to be determined by the courts. Standards set by standardization bodies or evolving out of the industry are of limited effect in the sense, that they normally constitute the minimum level, but do not prevent the courts requiring higher levels, what they do. The main problems assorted with software and artificial intelligence are the lack of transparency and related to this of predictability and reliability. But this no new problem to product liability where it is solved by duties to disclosure of evidence and a shift of the burden of proof, in the end making the producer accountable for the lack of transparency, predictability and reliability. There is some indication, that the product liability can cover the problems for responsibility and liability regarding software and artificial intelligence, maybe requiring some minor adaptions. The current discussion about introducing a new (strict) liability regime lacks a sufficient analysis of whether, where and why the existing regime is insufficient.

This presentation focuses on the integral role of expressive environment modeling tools within the realm of formal methods, underpinning the pursuit of verified AI. In this context, our research group at UC Berkeley has introduced Scenic, a probabilistic scenario description language designed to facilitate the realization of this goal. Scenic serves as a probabilistic programming language, enabling the formulation of distributions that characterize scenes and scenarios, the former representing configurations of physical objects and autonomous agents, and the latter encompassing distributions over these scenes and the dynamic behaviors of their constituent agents over time. This novel language is distinguished by its succinct and comprehensible syntax for spatiotemporal relationships, accompanied by the capacity to declaratively enforce both hard and soft constraints on the scenario. Furthermore, by considering accountability as an inherent system property, we find the application of Scenic crucial for precisely specifying the environmental conditions under which we can hold a software system accountable. In doing so, we illuminate the potential of Scenic as a means to enhance the accountability of software systems.

A computational system is called autonomous if it is able to make its own decisions, or take its own actions, without human supervision or control. The capability and spread of such systems have reached the point where they are beginning to touch much of everyday life. However, regulators grapple with how to deal with autonomous systems. We view certification of the behaviour of a system as, in appropriate cases, a component of accountability. This talk proposed to analyse what is needed in order to provide verified reliable behaviour of an autonomous system, analyse what can be done as the state-of-the-art in automated verification, and pointed to a roadmap towards developing regulatory guidelines, including articulating challenges to researchers, to engineers, and to regulators.