Verinec

If you are interested in reading one of our PhD thesis, please contact David for the thesis about Adaptation and Import and Dominik for the thesis about Verification and Simulation.

Publications & Conferences

• Improving Network Reliability by avoiding Misconfiguration
  David Buchmann, Dominik Jungo, Ulrich Ultes-Nitsche: DRCN 2007, La Rochelle, France, 7-10 October, 2007.

  To appear. Accepted for publication in June 2007

  Abstract: One source of network operation interruption is the human factor. In this paper, we discuss how network management systems can help to avoid mistakes in configuration. While ensuring correct syntax of configuration data is nothing novel, testing its semantics has become a challenge to network management.
  We illustrate possible solutions with the Verified Network Configuration (Verinec) project. A central XML database is used to model the network and device configuration. All configuration is tested before the setup of the real devices is modified.

• Assessment of code quality through classification of unit tests in VeriNeC
  Dominik Jungo, David Buchmann, Ulrich Ultes-Nitsche: AINA 2007, Niagara, Canada, May 21-23, 2007.

  Abstract: Unit testing is a tool for assessing code quality. Unit tests check the correctness of code fragments like methods, loops and conditional statements. Usually, every code fragment is involved in different tests. We propose a classification of tests, depending on the tested features, which delivers a higher detailed feedback than unclassified tests. Unclassified tests only deliver a feedback whether they failed or succeeded. The detailed feedback from the classified tests help to do a better code quality assessment and can be incorporated in tools helping to improve code quality. We demonstrate the power of this approach doing unit tests on network configuration.

• A role model to cope with the complexity of network configuration
  David Buchmann, Dominik Jungo, Ulrich Ultes-Nitsche: INOC 2007, Spa, Belgium, April 22-25, 2007.

  Abstract: In this paper, we propose a role model to cope with the complexity of network configuration. Roles associate policy requirements as well as configuration templates with nodes in the network. One goal is to remove redundancy in configuration data to avoid inconsistent changes and diverging setup of similar devices. The other goal is to ensure that network policies are respected by the configuration.
  This role model is embedded into the project Verified Network Configuration (Verinec). Together with the Verinec XML network model, roles provide a powerful instrument to configure large networks.

  Get the paper (PDF)

• Environmental Acquisition in Mobile Network Simulation
  David Buchmann, Dominik Jungo, Ulrich Ultes-Nitsche: WINSYS 2006, Setubal, Portugal August 2006.

  Abstract: The type or class of an object is not always sufficient to decide on its runtime behaviour. In many cases, the context of the object is also important. Environmental acquisition is a concept to handle context in information models.

  We explore the use of environmental acquisition for the management of computer network configuration and for network simulation. Physical location or subnet membership are part of the environment for a computer in a network. For the simulation of networks, environmental acquisition will be especially useful to model mobile devices moving from one area into an other. The concept is illustrated using the network configuration management project Verinec.

  Get the paper (PDF)

• CLiXML - Testing of semantic properties in XML documents
  Dominik Jungo, David Buchmann, Ulrich Ultes-Nitsche: MSVVEIS 2006, Cyprus May 23-24, 2006.

  Abstract: XML is a markup language with a clear hierarchical structure. Validating an XML document against a schema document is an important part in the work flow incorporating XML documents. Most approaches use grammar based schema languages. Grammar based schemas are well suited for the syntax definition of an XML document, but come to their limits when semantic properties are to be defined. This paper presents a rule based, first order schema language, complementary to grammar based schema languages, demonstrating its strength in defining semantic properties for an XML document.

• Automated Configuration Distribution in Verinec
  David Buchmann, Dominik Jungo, Ulrich Ultes-Nitsche: ICETE 2005, Reading, UK October 3-7, 2005.

  Abstract: We present in this paper a system to configure networks. The Verified Network Configuration (Verinec) project aims to manage the complete network from one central XML database. This approach allows to test whether the configuration is usable prior to modify the setup of the real network devices.

  The distribution of the configuration is handled by the adaption module, a framework which can be extended to support all kinds of services and devices. Applying the configuration to each managed device within the network requires conversion from the Verinec XML database into a format suitable for that device and send the configuration to the device using a protocol supported by that device. In this paper, we focus on the adaption module.

  Get the paper (PDF)

• A Unit Testing Framework for Network Configurations
  Dominik Jungo, David Buchmann, Ulrich Ultes-Nitsche: MSVVEIS 2005, Miami, USA May 24, 2005.

  Abstract: We present in this paper a unit testing framework for network configurations which verifies that the configuration meets prior defined requirements of the networks behavior. This framework increases the trust in the correctness, security and reliability of a networks configuration. Our testing framework is based on a behavioral simulation approach as it is used in hardware design.

  More Information...

• The Role of Simulation in a Network Configuration Engineering Approach
  Dominik Jungo, David Buchmann, Ulrich Ultes-Nitsche: ICICT 2004, Cairo, Egypt December 6-7, 2004.

  Abstract: We report in this paper on a network simulator, which allows checking behavioural properties of a network prior to the real configuration of the network. Properties such as filtering strategies of firewalls, the correct functionality of DNS or DHCP servers, etc. can be tested using the simulator. In the presented approach, the entire network configuration and topology is represented as eXtensible Markup Language (XML) documents, which the simulator reads and operates on accordingly. After successful tests of the network using the simulator, the XML configuration description will be translated automatically into configuration files that are used to configure the concrete services present in the actual network. The translation will be performed using eXtensible Stylesheet Language Transformations (XSLT).

  More Information...

• Intermediary report
  David Buchmann, 17.9.2004

  Abstract: The Verinec project aims to simplify network configuration. It is based upon an abstract definition of a network and the nodes in that network expressed in XML. Each node consists of its hardware (network interfaces) and a set of services such as DNS server, firewalls, and so on. The abstract configuration is translated automatically into configuration specific to the actual hard- and software used in the network. The simulator part of Verinec allows to check if the configuration will fullfill the desired behaviour prior to really configure the nodes. This paper describes the translation process.
  Keywords: Generating network configuration, network simulation, automated verification

Bachelor and Master thesis

For thesis currently offered or being worked on by a student, please see student projects list on the tns web site.

• GUI Base
  Renato Löffel, 2004

  Describes how the base framework of Verinec GUI has been designed. (However, the framework has been changed since this thesis)
  Paper in german.

• GUI Node Editor
  Damian Vogel, 2005

  Abstract: This thesis describes the environment and the development of a graphical user interface (GUI) which facilitates configuring computers in the network simulation and configuration program Verinec. This paper gives an overview of the functionality, the implementational choices and decisions, and the programming principles used in the code.

• Configuration Import
  Geraldine Antener, 2005

  Abstract: ConfigImporter is part of the VeriNeC project. VeriNeC aims to simplify the complex task of configuring a network. The core of VeriNeC is an abstract description of a network and its devices using XML. This abstract configuration can then be tested by means of simulation and translated to implementation specific configuration data. ConfigImporter imports the implementation specific configuration settings into the environment of the VeriNeC project. This paper shows how Linux (more precisely the distribution Fedora Red Hat) stores network configuration, and how these settings can be translated into VeriNeC's XML language.

• Sniffer
  Patrick Aebischer, 2005

  The sniffer module tries to determine an existing network setup by analysing the network traffic and using port scans on the hosts.
  Paper in german.

• Windows adapter
  Nadine Zurkinden, 2005

  Abstract: This paper shows how Windows machines can be remotely configured using a Java API. It is part of the project Verinec. Verinec aims to simplify network configuration. The idea is to describe the abstract definition of a network using the XML syntax. This abstract configuration will be translated automatically into machine specific configuration using XSLT. Then it will be distributed to the target system using the Windows Management Instrumentation (WMI). Through WMI, Windows resources can be managed locally or remotely over a network using scripts. The Java API used to access the WMI is Jawin. The configuration of the Ethernet card and dial-up modem was studied in detail. It was also researched, how the user account management is handled in Windows.
  Keywords: Network Configuration, Windows Management Instrumentation, Jawin

• Cisco Translator
  Christoph Ehret, 2005

  Abstract: This paper reports on my Master Thesis, which presents in a first part my observations on the way how the Simple Network Management Protocol is integrated in network devices, and in a second part my implementation of a Cisco translation service in the project called Verified Network Configuration (VeriNeC) [13] funded by the Swiss National Science Foundation. In today~s growing number of network devices, we really need an easy and efficient way to manage all these different devices. SNMP is theoretically a good candidate since it is the standard management protocol, but practically it is unfortunately misused by the network devices vendors. With VeriNeC, we can even go further than just management. The entire network definition and configuration is represented in an eXtensible Markup Language (XML) document which can be tested by its simulation module. After successful tests, the XML abstract definition of the network is translated into a configuration specific to a device and transfered to it. The translation is done using eXtensible Stylesheet Language Transformations (XSLT). In my work, we can see how to implement a translation service for Cisco.
  Keywords: VeriNeC, SNMP, Cisco, Ethernet, Packet-filters, Routing

• DJBDNS and DHCP translators
  Robert Awesso, 2005

  Abstract: Le but du projet VeriNeC est de simplier la conguration des réseaux. Il est basé sur la dénition d'un réseau abstrait et peut simuler diérents états d'un réseau tout comme générer des données de conguration pour le réseau. Le sous-projet ServiceTranslator s'occupe de la génération de chiers de conguration pour deux services dans le monde linux. Le service DNS et le service DHCP. Sachant que les chiers de conguration sont des chiers de texte et que le couple XML et XSLT peut donner n'importe quel type de document en sortie, nous voyons aisément toutes les possibilités qui nous sont données.
  Mots-clés : XML, XSLT, XML Schema, DNS, DHCP
  Paper in french.

• VeriNeC Firewall
  Jason Hug, 2006

  Abstract: In this report the implementation of a firewall for the Verified Network Configuration (VeriNeC) Simulator is discussed. The firewall simulates real life counterparts with a Packet- Filter and Stateful Inspection. Both components, which are based upon the IPTables implementation, were successfully integrated within the VeriNeC Simulator. How this was accomplished is described in this master thesis.

  Keywords: VeriNeC, Packet Filter, IPTables, Stateful Inspection, Network Simulation
  Paper in german.

• Traceroute for Network import
  Martial Seifriz, 2006

  Abstract: Diese Arbeit dokumentiert die Entwicklung und Verwendung des Network Importers für das VeriNeC Projekt. Ziel dieses Importers ist es, mittels Packet-Sniffer, Traceroute und Host-Scanner ein existierendes Netzwerk abzubilden und möglichst viele Informationen darüber zu sammeln, zu verarbeiten und zu speichern. VeriNeC soll es ermöglichen ein Netzwerk zuerst abstrakt zu konfigurieren und ausgiebig zu prüfen. Nach erfolgreichem Testen soll die erhaltene Konfiguration auf ein reales Netzwerk exportiert werden können. Damit ein existierendes Netzwerk in VeriNeC importiert werden kann, wurde bereits ein Packet-Sniffer implementiert, der einzelne Hosts in einem Netzwerk entdecken kann. Nachdem ein Host bekannt ist, können durch einen Port-Scanner die laufenden Dienste aufgelöst werden. Diese Arbeit dokumentiert nun, wie es möglich ist mittels Traceroute die Struktur eines Netzwerkes zu erhalten und abzubilden.
  Im folgenden soll ein Überblick über die Entwicklung, Implementation und Verwendung eines in Java geschriebenen Traceroute Package gegeben werden. Zudem wird dessen Einbindung und Verwendung im VeriNeC Importer erklärt werden.
  Paper in german.