No description available.

No description available.

The translation of binary code to higher-level models has wide applications, including decompilation, binary analysis, and binary rewriting. This calls for high reliability of the underlying trusted computing base (TCB) of the translation methodology. A key challenge is to reduce the TCB by validating its soundness. Both the definition of soundness and the validation method heavily depend on the context: what is in the TCB and how to prove it. This dissertation presents three research contributions. The first two contributions include reducing the TCB in binary verification, and the last contribution includes a binary verification process that leverages a reduced TCB. The first contribution targets the validation of OCaml-to-PVS translation -- commonly used to translate instruction-set-architecture (ISA) specifications to PVS -- where the destination language is non-executable. We present a methodology called OPEV to validate the translation between OCaml and PVS, supporting non-executable semantics. The validation includes generating large-scale tests for OCaml implementations, generating test lemmas for PVS, and generating proofs that automatically discharge these lemmas. OPEV incorporates an intermediate type system that captures a large subset of OCaml types, employing a variety of rules to generate test cases for each type. To prove the PVS lemmas, we develop automatic proof strategies and discharge the test lemmas using PVS Proof-Lite, a powerful proof scripting utility of the PVS verification system. We demonstrate our approach in two case studies that include 259 functions selected from the Sail and Lem libraries. For each function, we generate thousands of test lemmas, all of which are automatically discharged. The dissertation's second contribution targets the soundness validation of a disassembly process where the source language does not have well-defined semantics. Disassembly is a crucial step in binary security, reverse engineering, and binary verification. Various studies in these fields use disassembly tools and hypothesize that the reconstructed disassembly is correct. However, disassembly is an undecidable problem. State-of-the-art disassemblers suffer from issues ranging from incorrectly recovered instructions to incorrectly assessing which addresses belong to instructions and which to data. We present DSV, a systematic and automated approach to validate whether the output of a disassembler is sound with respect to the input binary. No source code, debugging information, or annotations are required. DSV defines soundness using a transition relation defined over concrete machine states: a binary is sound if, for all addresses in the binary that can be reached from the binary's entry point, the bytes of the (disassembled) instruction located at an address are the same as the actual bytes read from the binary. Since computing this transition relation is undecidable, DSV uses over-approximation by preventing false positives (i.e., the existence of an incorrectly disassembled reachable instruction but deemed unreachable) and allowing, but minimizing, false negatives. We apply DSV to 102 binaries of GNU Coreutils with eight different state-of-the-art disassemblers from academia and industry. DSV is able to find soundness issues in the output of all disassemblers. The dissertation's third contribution is WinCheck: a concolic model checker that detects memory-related properties of closed-source binaries. Bugs related to memory accesses are still a major issue for security vulnerabilities. Even a single buffer overflow or use-after-free in a large program may be the cause of a software crash, a data leak, or a hijacking of the control flow. Typical static formal verification tools aim to detect these issues at the source code level. WinCheck is a model-checker that is directly applicable to closed-source and stripped Windows executables. A key characteristic of WinCheck is that it performs its execution as symbolically as possible while leaving any information related to pointers concrete. This produces a model checker tailored to pointer-related properties, such as buffer overflows, use-after-free, null-pointer dereferences, and reading from uninitialized memory. The technique thus provides a novel trade-off between ease of use, accuracy, applicability, and scalability. We apply WinCheck to ten closed-source binaries available in a Windows 10 distribution, as well as the Windows version of the entire Coreutils library. We conclude that the approach taken is precise -- provides only a few false negatives -- but may not explore the entire state space due to unresolved indirect jumps. / Doctor of Philosophy / Binary verification is a process that verifies a class of properties, usually security-related properties, on binary files, and does not need access to source code. Since a binary file is composed of byte sequences and is not human-readable, in the binary verification process, a number of assumptions are usually made. The assumptions often involve the error-free nature of a set of subsystems used in the verification process and constitute the verification process's trusted computing base (or TCB). The reliability of the verification process therefore depends on how reliable the TCB is. The dissertation presents three research contributions in this regard. The first two contributions include reducing the TCB in binary verification, and the last contribution includes a binary verification process that leverages a reduced TCB. The dissertation's first contribution presents a validation on OCaml-to-PVS translations -- commonly used to translate a computer architecture's instruction specifications to PVS, a language that allows mathematical specifications. To build up a reliable semantical model of assembly instructions, which is assumed to be in the TCB, it is necessary to validate the translation. The dissertation's second contribution validates the soundness of the disassembly process, which translates a binary file to corresponding assembly instructions. Since the disassembly process is generally assumed to be trustworthy in many binary verification works, the TCB of binary verification could be reduced by validating the soundness of the disassembly process. With the reduced TCB, the dissertation introduces WinCheck, the dissertation's third and final contribution: a concolic model checker that validates pointer-related properties of closed-source Windows binaries. The pointer-related properties include absence of buffer overflow, absence of use-after-free, and absence of null-pointer dereference.

This thesis studies the relationship between the internal characteristics of the site, based on an existing set of artifacts, abandoned concrete railroad trestles, and external views of them. The project establishes orthogonal and non-orthogonal geometries in re-developing this urban site creating buildings that relate to the site, surroundings, and themselves. The physical, structural connections and spatial relationships reconcile the superimposition of geometries. Ultimately every decision in the project returns to the analysis of the site allowing for different buildings, people, and environments to interact as a single entity. / Master of Architecture

The rapid technological advancement in the past century resulted in a decreased life cycle of a large number of products and, consequently, increased the rate of technological obsolescence. The disposal of obsolete products has resulted in rapid landfilling and now poses a major environmental threat. The governments in many countries around the world have started imposing regulations to curb uncontrolled product disposal. The consumers, too, are now aware of adverse effects of product disposal on environment and increasingly favor environmentally benign products. In the wake of imminent stringent government regulations and the consumer awareness about ecosystem-friendly products, the manufacturers need to think about the alternatives to product disposal. One way to deal with this problem is to disassemble an obsolete product and utilize some of its components/subassemblies in the manufacturing of new products. This seems to be a promising solution because products now-a-days are made in accordance with the highest quality standards and, although an obsolete product may not be in the required functional state as a whole, it is possible that several of its components or subassemblies are still in near perfect condition. However, product disassembly is a complex task requiring human labor as well as automated processes and, consequently, a huge amount of monetary investment. This research addresses a disassembly optimization problem, which aims at minimizing the costs associated with the disassembly process (namely, the costs of breaking the joints and the sequence dependent set-up cost associated with disassembly operations), while maximizing the benefits resulting from recovery of components/subassemblies from a product. We provide a mathematical abstraction of the disassembly optimization problem in the form of integer-programming models. One of our formulations includes a new way of modeling the subtour elimination constraints (SECs), which are usually encountered in the well-known traveling salesman problems. Based on these SECs, a new valid formulation for asymmetric traveling salesman problem (ATSP) was developed. The ATSP formulation was further extended to obtain a valid formulation for the precedence constrained ATSP. A detailed experimentation was conducted to compare the performance of the proposed formulations with that of other well-known formulations discussed in the literature. Our results indicate that in comparison to other well-known formulations, the proposed formulations are quite promising in terms of the LP relaxation bounds obtained and the number of branch and bound nodes explored to reach an optimal integer solution. These new formulations along with the results of experimentation are presented in Appendix A. To solve the disassembly optimization problem, a three-phase iterative solution procedure was developed that can determine optimal or near optimal disassembly plans for complex assemblies. The first phase helps in obtaining an upper bound on our maximization problem through an application of a Lagrangian relaxation scheme. The second phase helps to further improve this bound through addition of a few valid inequalities in our models. In the third phase, we fix some of our decision variables based on the solutions obtained in the iterations of phases 1 and 2 and then implement a branch and bound scheme to obtain the final solution. We test our procedure on several randomly generated data sets and identify the factors that render a problem to be computationally difficult. Also, we establish the practical usefulness of our approach through case studies on the disassembly of a computer processor and a laser printer. / Master of Science

Yes / The physical properties of cyclic and linear polymers are markedly different; however, there are few examples which exploit these differences in clinical applications. In this study, we demonstrate that self-assemblies comprised of cyclic-linear graft copolymers are significantly more stable than the equivalent linear-linear graft copolymer assemblies. This difference in stability can be exploited to allow for triggered disassembly by cleavage of just a single bond within the cyclic polymer backbone, via disulfide reduction, in the presence of intracellular levels of l-glutathione. This topological effect was exploited to demonstrate the first example of topology-controlled particle disassembly for the controlled release of an anti-cancer drug in vitro. This approach represents a markedly different strategy for controlled release from polymer nanoparticles and highlights for the first time that a change in polymer topology can be used as a trigger in the design of delivery vehicles. We propose such constructs, which demonstrate disassembly behavior upon a change in polymer topology, could find application in the targeted delivery of therapeutic agents. / ERC are acknowledged for support to M.C.A., A.P.D. (grant number: 681559) and R.O.R. (grant number: 615142).

This report presents a master’s thesis in Industrial Design Engineering at KTH Royal Institute of Technology in Stockholm. The project was conducted on behalf of Silva Sweden AB during the spring of 2023, with the goal of modularizing Silva’s current assortment of land compasses. The objectives included reducing the number of components and improving repairability while contributing to Silva’s sustainability framework. Additional objectives were to redesign vital components in order to enable a modular system that is implementable in a circular business model, benefiting both customers and Silva. The methodology of this project included researching, collecting data, mapping, testing and evaluating, ideating, developing, finalizing and communicating. Moreover, the focuses of this project have been the development of baseplates, the compass housing assembly and the mirror attachment. The final design and new compass assortment resulted in a reduction of 40 % of the total components. The most influencing factors for the reduction, besides standardization, were an improved housing assembly and a solution that joins the regular baseplate with a detachable mirror through a snap fit. In relation to the purpose of this project, all objectives are concluded as fulfilled as well as the deliverables which are successfully achieved as well. In conclusion, the result of this project provides a new and modular compass design that minimizes the number of components while contributing to the development of a sustainable compass assortment. / Detta är en masteruppsats inom Teknisk Design vid KTH Kungliga Tekniska Högskolan i Stockholm. Projektet genomfördes under våren 2023 på uppdrag av Silva Sweden AB med målet att modularisera Silvas befintliga sortiment av landkompasser. Syftet med projektet inkluderade minskning av antalet komponenter samt att utöka möjligheten för reparation av kompasser, och således bidra till Silvas pågående hållbarhetsarbete. Lösningen bör även möjliggöra ett modulärt system som ska kunna implementeras i en cirkulär affärsmodell till förmån för både kunder och Silva som företag. Metodiken i detta projekt inkluderade forskning, datainsamling, kartläggning, testning och utvärdering, idégenerering, utveckling, avslutning och kommunikation. Fokus för detta projekt varit att utveckla basplattan, nålhuset och spegelfästet. Den slutliga designen och det nya kompass sortimentet resulterade i en minskning på 40% av det totala antalet komponenter. De mest avgörande faktorerna för minskningen var den modulära lösningen som kombinerade den vanliga basplattan med en avtagbar spegel, samt standardiseringen av komponenter i det nya nålhuset. Utifrån de syften och mål som definierades i projektet så påvisar den slutgiltiga designen att alla dessa är uppfyllda. Sammanfattningsvis visar projektets resultat en ny och modulär kompassdesign som minskar antalet komponenter samtidigt som den bidrar till utvecklingen av ett hållbart kompass sortiment.

La réalité des marchés économiques impose des contraintes aux entreprises manufacturières qui sont de plus en plus difficiles à réaliser, comme la diversification des produits, l'amélioration de leur qualité, la réduction des coûts et la diminution des retards. Ces contraintes sont satisfaites par une meilleure organisation des systèmes de fabrication en utilisant les ressources techniques existantes. Notre présente thèse met l’accent sur deux contributions majeures, la première consiste à modéliser différents cas du système industriel (Système de production simple, système d’assemblage, système de désassemblage) en intégrant des politiques de maintenance adéquates. La deuxième contribution repose sur l’évaluation des risques de pertes de profit d’une décision prise suite à l’optimisation des différents systèmes industriels étudiés. Trois différents problèmes industriels sont étudiés, le premier concerne le développement des méthodes d’évaluation de risque de perte de profit résultant du choix d'un algorithme d’optimisation pour résoudre un problème de planification conjointe de production et de maintenance. Pour atteindre nos objectifs, nous commençons par calculer les plans de production et de maintenance en utilisant différents algorithmes d’optimisation. En outre, nous proposons des modèles analytiques pour quantifier le risque de perte de profit résultant des retours de produits et de la prise en compte des durées de réparation de pannes non nulles. Cette étude fournit des informations sur les algorithmes d’optimisations les plus efficaces pour les problématiques rencontrés pour aider et orienter les décideurs dans l'analyse et l'évaluation de leurs décisions. La deuxième problématique concerne l'optimisation de la planification du système d'assemblage à deux niveaux. Un modèle mathématique est développé pour incorporer une planification de l'approvisionnement pour les systèmes d'assemblage à deux niveaux dont les délais d’approvisionnement et les pannes du système sont stochastiques. La planification de maintenance optimale obtenue est utilisée dans l'évaluation des risques afin de trouver la période seuil de réparation qui réduit les pertes de profit. La troisième problématique étudiée concerne l’optimisation de la planification dans le cadre d’assemblage à base de désassemblage des produits usagés en tenant compte de la dégradation du système de production. Un modèle analytique est développé pour envisager le désassemblage, la remise à neuf des produits usagés qui contribuent à l’assemblage des produits finis. En effet, ces derniers peuvent être constitués de composants neufs ou remis à neuf. Une politique de maintenance est séquentiellement intégrée pour réduire l'indisponibilité du système. Le but de cette étude est d'aider les décideurs, dans certaines conditions, à choisir le processus le plus rentable pour satisfaire le client et qui peut également s'adapter aux risques potentiels qui peuvent perturber le système de désassemblage-assemblage. Le risque lié aux périodes de réparation du système est discuté, ce qui a un impact sur la prise de décision managériale / The reality of the economic markets places constraints on manufacturing companies that are increasingly difficult to achieve, such as product diversification, quality improvement, cost reduction and fewer delays. These constraints are satisfied by a better organization of manufacturing systems using existing technical resources. Our thesis focuses on two major contributions, the first is to model different industrial systems (simple production system, assembly system, disassembly system) by integrating maintenance policies. The second contribution is based on risk assessment of profit loss following a decision taken after an optimization of an industrial system. Three different industrial problems are studied; the first concerns the development of risk assessment methods of profit loss resulting from the choice of an optimization algorithm to solve a problem of joint production and maintenance planning. To achieve our goals, we start by calculating production and maintenance plans using different optimization algorithms. In addition, we propose analytical models to quantify the risk of profit loss resulting from product returns and of repair times. This study provides information on the most effective optimization algorithms for the problems encountered to help and guide decision-makers in the analysis and evaluation of their decisions. The second problem concerns the optimization of two-level assembly system planning. A mathematical model is developed to incorporate supply planning for two-level assembly system with stochastic lead times and failures. The optimal maintenance planning obtained is used in the risk assessment to find the threshold repair period that reduces the profit loss. The third problem studied concerns the optimization of disassembly system of returned products (used or end of life products), remanufacturing and assembly of finished products taking into account the degradation of the production system. An analytical model is developed to consider disassembly, remanufacturing of returned products that contribute to the assembly of finished products. Indeed, the latter may consist of new or remanufactured components. A maintenance policy is sequentially integrated to reduce the unavailability of the system. The goal of this study is to help decision makers, under certain conditions, choose the most cost-effective process to satisfy the customer and who can also adapt to the potential risks that can disrupt the disassembly-remanufacturing-assembly system. The risk associated with system repair periods is discussed, which has an impact on managerial decision-making

No description available.

Durant les dernières décennies, des réseaux de logistiques inverses ont été lancésdans plusieurs pays industrialisés dans l’objectif de préserver l’environnement. La mise enplace et la gestion de cette logistique concernent les différents niveaux, stratégique, tactique etopérationnel existants dans le cadre de la logistique directe pour tout système de productionde biens industriels. Pour améliorer ce type de réseau, la modélisation et la simulation sontdes outils efficaces. Après avoir présenté un état de l’art de ce domaine, notre étude sefocalise sur la planification de certains sous-ensembles (appelés maillons) de cette chaineinverse (i.e. collecte-tri, désassemblage) au niveau tactique, c'est-à-dire à moyen terme. Lebut de ce travail est donc de proposer un modèle générique en programmation linéaire dans uncontexte multi-produit et multi-période, qui cherche à maximiser le profit total du maillonétudié et qui prend en compte l’incertitude sur la qualité des produits traités. Le modèlelinéaire en nombres entiers (déterministe, stochastique et évaluation stochastique) est ainsiformulé autour d’un profit contraint par les capacités du maillon, l’évolution des stocksentrants et sortants et la livraison des produits traités aux clients, avec une politique delivraison sans déclassement ou avec déclassement des produits. / During the last decades, reverse logistics networks have been launched in severalindustrialized countries with the aim of preserving the environment. The implementation andmanagement of the reverse logistics concerns the different levels (strategic, tactical andoperational) existing in the framework of forward logistics for any production system. Toimprove this type of network, modeling and simulation are effective tools. After presenting astate of the art in this domain, our study focuses on the planning of two sub-systems of thereverse logistics chain (i.e. collection-sorting and disassembly) on the tactical level that is tosay the medium term. The aim of this work is to propose a generic model by linearprogramming in a multi-product and multi-period context, which searches for maximizingthe total profit of the sub-system studied, taking into account the uncertainty of the productssupplied. The integer linear model (deterministic, stochastic and stochastic assessment) is thusformulated around a profit constrained by the sub-system capacity, the evolution of incomingand outgoing inventory and the delivery of products to customers: a delivery policyauthorizing the quality degrading of products or not.