Die vorliegende Arbeit beschäftigt sich mit der technischen Sicherheit (engl. Safety) sowie der Informationssicherheit (engl. Security) von Programmen. Im Speziellen betrachten wir die Korrektheit von SiJa-Programmen, einer Teilmenge von Java, im Quellcode und dem daraus erzeugten Java-Bytecode. In der aktuellen Forschung werden die einzelnen Aspekte fast ausschließlich getrennt behandelt. Das heißt, es wird nur die technische Sicherheit oder nur die Informationssicherheit von Programmen betrachtet und dann entweder nur mit Bezug auf den Quellcode oder nur für das kompilierte Programm. Wir schlagen stattdessen ein Rahmenwerk vor, das die unterschiedlichen Aspekte in einem einzigen Prozess vereint. Die Grundidee des Rahmenwerks ist ein einheitlicher Ansatz zur beweisbar korrekten Programmtransformation unter Anwendung von Techniken aus der Deduktion sowie der symbolischen Programmausführung. Mithilfe von KeY werden die SiJa-Programme (im Quellcode) verifiziert und deren Korrektheit sichergestellt. Die Verifikationstechnik beruht auf symbolischer Ausführung. Um die Korrektheitsbeweise klein zu halten, werden abwechselnd Programmspezialisierungsschritte und symbolische Ausführungsschritte angewendet. Aus dem während der Verifikationsphase konstruierten symbolischen Ausführungsbaum erzeugen wir ein zum Ursprungsprogramm bezüglich des beobachtbaren Programmzustandes äquivalentes und optimiertes transformiertes Programm. Die Korrektheit der Programmtransformation wird in dieser Arbeit bewiesen. Ferner wenden wir diesen Ansatz an, um ein Programm zu generieren, welches bezüglich Variablen mit einer niedrigen Sicherheitsstufe das gleiche Verhalten aufweist wie das ursprüngliche Programm. Damit ist es uns möglich eine präzisiere Informationsflussanalyse zu realisieren als vergleichbare typ-basierte Systeme. Des weiteren erlaubt das Rahmenwerk SiJa-Quellcode in Java-Bytecode zu kompilieren, ohne das dessen Korrektheit bewiesen werden muss, da sie aus der Verifikation des Quellcodes folgt. Insbesondere ist dank unseres Ansatzes eine Verifikation des Compilers nicht notwendig.