@misc{LorenzKiekhebenSchnor2017, author = {Lorenz, Claas and Kiekheben, Sebastian and Schnor, Bettina}, title = {FaVe: Modeling IPv6 firewalls for fast formal verification}, series = {International Conference on Networked Systems (NetSys) 2017}, journal = {International Conference on Networked Systems (NetSys) 2017}, publisher = {IEEE}, address = {New York}, doi = {10.1109/NetSys.2017.7903956}, pages = {8}, year = {2017}, abstract = {As virtualization drives the automation of networking, the validation of security properties becomes more and more challenging eventually ruling out manual inspections. While formal verification in Software Defined Networks is provided by comprehensive tools with high speed reverification capabilities like NetPlumber for instance, the presence of middlebox functionality like firewalls is not considered. Also, they lack the ability to handle dynamic protocol elements like IPv6 extension header chains. In this work, we provide suitable modeling abstractions to enable both - the inclusion of firewalls and dynamic protocol elements. We exemplarily model the Linux ip6tables/netfilter packet filter and also provide abstractions for an application layer gateway. Finally, we present a prototype of our formal verification system FaVe.}, language = {en} } @misc{GawronChengMeinel2017, author = {Gawron, Marian and Cheng, Feng and Meinel, Christoph}, title = {PVD: Passive Vulnerability Detection}, series = {8th International Conference on Information and Communication Systems (ICICS)}, journal = {8th International Conference on Information and Communication Systems (ICICS)}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5090-4243-2}, issn = {2471-125X}, doi = {10.1109/IACS.2017.7921992}, pages = {322 -- 327}, year = {2017}, abstract = {The identification of vulnerabilities relies on detailed information about the target infrastructure. The gathering of the necessary information is a crucial step that requires an intensive scanning or mature expertise and knowledge about the system even though the information was already available in a different context. In this paper we propose a new method to detect vulnerabilities that reuses the existing information and eliminates the necessity of a comprehensive scan of the target system. Since our approach is able to identify vulnerabilities without the additional effort of a scan, we are able to increase the overall performance of the detection. Because of the reuse and the removal of the active testing procedures, our approach could be classified as a passive vulnerability detection. We will explain the approach and illustrate the additional possibility to increase the security awareness of users. Therefore, we applied the approach on an experimental setup and extracted security relevant information from web logs.}, language = {en} } @misc{MuehlbauerSchroederSkoncejetal.2017, author = {M{\"u}hlbauer, Felix and Schr{\"o}der, Lukas and Skoncej, Patryk and Sch{\"o}lzel, Mario}, title = {Handling manufacturing and aging faults with software-based techniques in tiny embedded systems}, series = {18th IEEE Latin American Test Symposium (LATS 2017)}, journal = {18th IEEE Latin American Test Symposium (LATS 2017)}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5386-0415-1}, doi = {10.1109/LATW.2017.7906756}, pages = {6}, year = {2017}, abstract = {Non-volatile memory area occupies a large portion of the area of a chip in an embedded system. Such memories are prone to manufacturing faults, retention faults, and aging faults. The paper presents a single software based technique that allows for handling all of these fault types in tiny embedded systems without the need for hardware support. This is beneficial for low-cost embedded systems with simple memory architectures. A software infrastructure and a flow are presented that demonstrate how the presented technique is used in general for fault handling right after manufacturing and in-the-field. Moreover, a full implementation is presented for a MSP430 microcontroller, along with a discussion of the performance, overhead, and reliability impacts.}, language = {en} } @misc{MuehlbauerSchroederSchoelzel2017, author = {M{\"u}hlbauer, Felix and Schr{\"o}der, Lukas and Sch{\"o}lzel, Mario}, title = {On hardware-based fault-handling in dynamically scheduled processors}, series = {20th International Symposium on Design and Diagnostics of Electronic Circuits \& Systems (DDECS) 2017}, journal = {20th International Symposium on Design and Diagnostics of Electronic Circuits \& Systems (DDECS) 2017}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5386-0472-4}, issn = {2334-3133}, doi = {10.1109/DDECS.2017.7934572}, pages = {201 -- 206}, year = {2017}, abstract = {This paper describes architectural extensions for a dynamically scheduled processor, so that it can be used in three different operation modes, ranging from high-performance, to high-reliability. With minor hardware-extensions of the control path, the resources of the superscalar data-path can be used either for high-performance execution, fail-safe-operation, or fault-tolerant-operation. This makes the processor-architecture a very good candidate for applications with dynamically changing reliability requirements, e.g. for automotive applications. The paper reports the hardware-overhead for the extensions, and investigates the performance penalties introduced by the fail-safe and fault-tolerant mode. Furthermore, a comprehensive fault simulation was carried out in order to investigate the fault-coverage of the proposed approach.}, language = {en} } @misc{MalchowRenzBaueretal.2017, author = {Malchow, Martin and Renz, Jan and Bauer, Matthias and Meinel, Christoph}, title = {Embedded smart home}, series = {11th Annual IEEE International Systems Conference (SysCon)}, journal = {11th Annual IEEE International Systems Conference (SysCon)}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5090-4623-2}, issn = {1944-7620}, doi = {10.1109/SYSCON.2017.7934728}, pages = {195 -- 200}, year = {2017}, abstract = {The popularity of MOOCs has increased considerably in the last years. A typical MOOC course consists of video content, self tests after a video and homework, which is normally in multiple choice format. After solving this homeworks for every week of a MOOC, the final exam certificate can be issued when the student has reached a sufficient score. There are also some attempts to include practical tasks, such as programming, in MOOCs for grading. Nevertheless, until now there is no known possibility to teach embedded system programming in a MOOC course where the programming can be done in a remote lab and where grading of the tasks is additionally possible. This embedded programming includes communication over GPIO pins to control LEDs and measure sensor values. We started a MOOC course called "Embedded Smart Home" as a pilot to prove the concept to teach real hardware programming in a MOOC environment under real life MOOC conditions with over 6000 students. Furthermore, also students with real hardware have the possibility to program on their own real hardware and grade their results in the MOOC course. Finally, we evaluate our approach and analyze the student acceptance of this approach to offer a course on embedded programming. We also analyze the hardware usage and working time of students solving tasks to find out if real hardware programming is an advantage and motivating achievement to support students learning success.}, language = {en} } @misc{Angerer2017, author = {Angerer, Marie-Luise}, title = {Moving Forces}, series = {The minnesota review}, volume = {88}, journal = {The minnesota review}, publisher = {Duke Univ. Press}, address = {Durham}, issn = {0026-5667}, doi = {10.1215/00265667-3787414}, pages = {83 -- 95}, year = {2017}, abstract = {Throughout a large part of the twentieth century, the body was interpreted as a field of signs, the meaning of which pointed to an unconscious dimension. At the height of the popularity of structuralism, Jacques Lacan deemed the unconscious to be "structured like a language." Starting in the early 1990s, however, a deep shift occurred in the way the body was interpreted. A new movement cast tremendous doubt on the hegemony of language and instead advocated a performative, pictorial, and affective approach — the so-called material turn — which encompassed all of these. In the words of Karen Barad, this turn inquired as to why meaning, history, and truth are assigned to language only, whereas the movements of materiality are given less prominence: "How did language come to be more trustworthy than matter? Why are language and culture granted their own agency and historicity while matter is figured as passive and immutable?" With this shift toward the material, bodies began to be seen in a different light and their materiality understood as something that follows its own laws and movements, which cannot be understood exclusively in terms of social-cultural codes. Instead, these laws and movements call into question the very dichotomies of nature/culture and body/spirit.}, language = {en} } @misc{NeubauerWankoSchaubetal.2017, author = {Neubauer, Kai and Wanko, Philipp and Schaub, Torsten H. and Haubelt, Christian}, title = {Enhancing symbolic system synthesis through ASPmT with partial assignment evaluation}, series = {Proceedings of the Design, Automation \& Test in Europe Conference \& Exhibition (DATE), 2017}, journal = {Proceedings of the Design, Automation \& Test in Europe Conference \& Exhibition (DATE), 2017}, publisher = {IEEE}, address = {New York}, isbn = {978-3-9815370-9-3}, issn = {1530-1591}, doi = {10.23919/DATE.2017.7927005}, pages = {306 -- 309}, year = {2017}, abstract = {The design of embedded systems is becoming continuously more complex such that efficient system-level design methods are becoming crucial. Recently, combined Answer Set Programming (ASP) and Quantifier Free Integer Difference Logic (QF-IDL) solving has been shown to be a promising approach in system synthesis. However, this approach still has several restrictions limiting its applicability. In the paper at hand, we propose a novel ASP modulo Theories (ASPmT) system synthesis approach, which (i) supports more sophisticated system models, (ii) tightly integrates the QF-IDL solving into the ASP solving, and (iii) makes use of partial assignment checking. As a result, more realistic systems are considered and an early exclusion of infeasible solutions improves the entire system synthesis.}, language = {en} } @misc{StaubitzWilkinsHagedornetal.2017, author = {Staubitz, Thomas and Wilkins, Christian and Hagedorn, Christiane and Meinel, Christoph}, title = {The Gamification of a MOOC Platform}, series = {Proceedings of 2017 IEEE Global Engineering Education Conference (EDUCON)}, journal = {Proceedings of 2017 IEEE Global Engineering Education Conference (EDUCON)}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5090-5467-1}, issn = {2165-9567}, doi = {10.1109/EDUCON.2017.7942952}, pages = {883 -- 892}, year = {2017}, abstract = {Massive Open Online Courses (MOOCs) have left their mark on the face of education during the recent years. At the Hasso Plattner Institute (HPI) in Potsdam, Germany, we are actively developing a MOOC platform, which provides our research with a plethora of e-learning topics, such as learning analytics, automated assessment, peer assessment, team-work, online proctoring, and gamification. We run several instances of this platform. On openHPI, we provide our own courses from within the HPI context. Further instances are openSAP, openWHO, and mooc.HOUSE, which is the smallest of these platforms, targeting customers with a less extensive course portfolio. In 2013, we started to work on the gamification of our platform. By now, we have implemented about two thirds of the features that we initially have evaluated as useful for our purposes. About a year ago we activated the implemented gamification features on mooc.HOUSE. Before activating the features on openHPI as well, we examined, and re-evaluated our initial considerations based on the data we collected so far and the changes in other contexts of our platforms.}, language = {en} } @article{Haag2017, author = {Haag, Johannes}, title = {A kantian critique of sellars transcendental realism}, series = {Wilfrid Sellars, Idealism, and Realism: Understanding Psychological Nominalism}, journal = {Wilfrid Sellars, Idealism, and Realism: Understanding Psychological Nominalism}, publisher = {Bloomsbury}, address = {London}, isbn = {978-1-4742-3895-3}, pages = {149 -- 171}, year = {2017}, language = {en} } @article{MeerReichardRingeling2017, author = {Meer, Frans-Bauke van der and Reichard, Christoph and Ringeling, Arthur}, title = {Becoming a Student of Reform}, series = {Theory and practice of public sector reform}, volume = {27}, journal = {Theory and practice of public sector reform}, publisher = {Routledge}, address = {New York}, isbn = {978-1-315-71414-1}, pages = {265 -- 283}, year = {2017}, language = {en} }