Durchsetzung und Analyse von Programmierrichtlinien für sichere Web-Programmierung mit Typsystemen

• Antragsteller: Dr. Ulrich Schöpp
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Theoretische Informatik
• Förderung: Förderung von 2014 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 250888164

Moderne Software muss typischerweise mit der ganzen Welt interagieren. Während bis vor kurzem solche weltweite Interaktion relativ selten war, so hat heute fast jede Unternehmenssoftware eine Web-Schnittstelle, welche es jeder beliebigen Person erlaubt, mit der Software zu interagieren und sei es nur durch die Eingabe eines falschen Passworts. Da das erforderliche Spezialwissen und die entsprechende Erfahrung im Umgang mit solchen Risiken i.a. nicht ausreichend vorhanden sind, wurden Richtlinien entwickelt, die das Expertenwissen zusammenfassen und einem größeren Personenkreis zur Verfügung stellen (Schlagwort "Sichere Programmierung"). Ob allerdings solche Richtlinien angewendet werden und ob dies in korrekter Weise geschieht, bleibt der Verantwortung der Programmierer überlassen. In diesem Projekt sollen automatische, auf Typsystemen beruhende, Methoden entwickelt werden, mit denen geprüft werden kann, ob eine gegebene Richtlinie korrekt und sinnvoll angewendet wurde und dies ohne die Flexibilität bei der Softwareentwicklung zu stark zu beeinträchtigen. Neben methodischen Weiterentwicklungen auf dem Gebiet der Typsysteme erfordert dies den Entwurf eines Formalismus indem solche Richtlinien, welche ja üblicherweise in informellem Englisch und mithilfe von Beispielen formuliert sind, rigoros festgelegt werden können. Damit Anwender diesem System vertrauen und es als nützliches Werkzeug wahrnehmen wird es notwendig sein, einen sehr hohen Genauigkeitsgrad zu erreichen. Wird etwa eine bereits aufgrund einer Richtlinie korrekt vorverarbeitete Benutzereingabe in einem Puffer gespeichert und später wieder ausgelesen, so ist es natürlich nicht nötig, sie erneut vorzuverarbeiten. Wenn das automatische System solch eine Situation nicht erkennt, so werden Anwender dazu neigen, seine Warnungen nicht ernstzunehmen. Ähnlich verhält es sich, wenn erforderliche Autorisierungen wie üblich durch Klasseninvarianten sichergestellt werden. Das bedeutet, dass neueste Techniken, wie etwa genaue Analyse von Zeichenketten, Objekten, Kontrollfluss und Aufrufkontexten zum Einsatz kommen und noch weiterentwickelt werden müssen. Um entsprechende Rückmeldungen und nahtlose Integration unterschiedlicher Methoden zu ermöglichen, werden wir typentheoretische Formulierungen derselben einsetzen, was in einem konfigurierbaren Typsystem aus einem Guss resultieren wird, welches in der Lage ist, ein breites Spektrum von Richtlinien für sichere Web-Programmierung abzubilden. Als Leitbeispiel sollen mit Codeinjektion (wie z.B. XSS) verbundene Richtlinien dienen, die sicherstellen, dass in Benutzereingaben möglicherweise enthaltene Codefragmente nicht ungewollt ausgeführt werden. Weitere Beispiele ergeben sich über Industriekontakte und aus einschlägigen WWW-Plattformen wie OWASP und SANS. Die hauptsächlichen wissenschaftlichen Innovationen sind die Fokussierung auf Richtlinien anstatt auf Risiken wie bisher üblich und die Entwicklung eines frei konfigurierbaren Typsystems.

• DFG-Verfahren: Sachbeihilfen
• Mitverantwortlich: Dr. Steffen Jost