SecureRandom.mark

// SPDX-License-Identifier: Apache-2.0

/*
 * Copyright (c) 2020-2023, Fraunhofer AISEC. All rights reserved.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      https://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 *
 *     _____          _
 *    / ____|        | |
 *   | |     ___   __| |_   _ _______
 *   | |    / _ \ / _` | | | |_  / _ \
 *   | |___| (_) | (_| | |_| |/ /  __/
 *    \_____\___/ \__,_|\__, /___\___|
 *                      __/ |
 *                     |___/
 */
package java.jca

entity SecureRandom {

    var algorithm;
    var provider;
    var params;
    var seed;
    var numBytes;
    var randomBytes;

    op instantiate {
        java.security.SecureRandom.getInstance(algorithm : java.lang.String);
        java.security.SecureRandom.getInstance(
            algorithm : java.lang.String,
            provider : java.lang.String | java.security.Provider
        );
        java.security.SecureRandom.getInstance(
            algorithm : java.lang.String,
            params : java.security.SecureRandomParameters
        );
        java.security.SecureRandom.getInstance(
            algorithm : java.lang.String,
            params : java.security.SecureRandomParameters,
            provider : java.lang.String | java.security.Provider
        );
        java.security.SecureRandom.getInstanceStrong();
        
        // forbidden calls because they don't respect BC as provider
        forbidden java.security.SecureRandom();
        forbidden java.security.SecureRandom(
            seed : byte[]
        );
    }

    op seed {
        java.security.SecureRandom.setSeed(seed : byte[] | long);
    }

    op reseed {
        java.security.SecureRandom.reseed();
        java.security.SecureRandom.reseed(params : java.security.SecureRandomParameters);
    }

    op generateSeed {
        seed = java.security.SecureRandom.generateSeed(numBytes : int);
    }

    op generate {
        java.security.SecureRandom.next(numBytes : int);
        java.security.SecureRandom.nextBytes(randomBytes : bytes[]);
        java.security.SecureRandom.nextBytes(
            randomBytes : bytes[],
            params : java.security.SecureRandomParameters
        );
    }
}